chore(Algebra/Group/Subgroup/Pointwise.lean): remove one hypothesis from Subgroup.closure_pow_le (leanprover-community#33401)

Remove the hypothesis on `n` from `Subgroup.closure_pow_le`

Author: AntoineChambert-Loir

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

@@ -223,19 +223,13 @@ theorem closure_mul_le (S T : Set G) : closure (S * T) ≤ closure S ⊔ closure
       (SetLike.le_def.mp le_sup_right <| subset_closure ht)
 
 @[to_additive]
-lemma closure_pow_le : ∀ {n}, n ≠ 0 → closure (s ^ n) ≤ closure s
-  | 1, _ => by simp
-  | n + 2, _ =>
-    calc
-      closure (s ^ (n + 2))
-      _ = closure (s ^ (n + 1) * s) := by rw [pow_succ]
-      _ ≤ closure (s ^ (n + 1)) ⊔ closure s := closure_mul_le ..
-      _ ≤ closure s ⊔ closure s := by gcongr ?_ ⊔ _; exact closure_pow_le n.succ_ne_zero
-      _ = closure s := sup_idem _
+lemma closure_pow_le : ∀ {n}, closure (s ^ n) ≤ closure s
+  | 0 => by simp_all
+  | n + 1 => by grw [pow_succ, closure_mul_le, closure_pow_le, sup_idem]
 
 @[to_additive]
 lemma closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
-  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn
+  closure_pow_le.antisymm <| by gcongr; exact subset_pow hs hn
 
 @[to_additive]
 theorem sup_eq_closure_mul (H K : Subgroup G) : H ⊔ K = closure ((H : Set G) * (K : Set G)) :=