feat(Perm/Fin): generalize sign_finRotate (leanprover-community#39209)

Author: urkud

Mathlib/GroupTheory/Perm/Fin.lean

@@ -92,12 +92,15 @@ theorem finRotate_succ_eq_decomposeFin {n : ℕ} :
       swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]
 
 @[simp]
-theorem sign_finRotate (n : ℕ) : Perm.sign (finRotate (n + 1)) = (-1) ^ n := by
-  induction n with
+theorem sign_finRotate (n : ℕ) : Perm.sign (finRotate n) = (-1) ^ (n - 1) := by
+  cases n with
   | zero => simp
-  | succ n ih =>
-    rw [finRotate_succ_eq_decomposeFin]
-    simp [ih, pow_succ]
+  | succ n =>
+    induction n with
+    | zero => simp
+    | succ n ih =>
+      rw [finRotate_succ_eq_decomposeFin]
+      simp [ih, pow_succ]
 
 @[simp]
 theorem support_finRotate {n : ℕ} : support (finRotate (n + 2)) = Finset.univ := by

Mathlib/GroupTheory/SpecificGroups/Alternating.lean

@@ -105,7 +105,7 @@ theorem IsThreeCycle.mem_alternatingGroup {f : Perm α} (h : IsThreeCycle f) :
 
 theorem finRotate_bit1_mem_alternatingGroup {n : ℕ} :
     finRotate (2 * n + 1) ∈ alternatingGroup (Fin (2 * n + 1)) := by
-  rw [mem_alternatingGroup, sign_finRotate, pow_mul, pow_two, Int.units_mul_self, one_pow]
+  simp [mem_alternatingGroup]
 
 end Equiv.Perm