refactor: Redefine pow in terms of iterate

In the `Monoid` instances for `Function.End α`, `Equiv.Perm α`, `AddMonoid.End α`, `α →+* α`, replace the default `npowRec` by a custom one in terms of `Nat.iterate`. Write the expected coercion lemmas.

As a consequence, I can delete the recently introduced file `Algebra.Ring.Hom.IterateHom`.

Author: YaelDillies

Mathlib.lean

@@ -576,7 +576,6 @@ import Mathlib.Algebra.Ring.Equiv
 import Mathlib.Algebra.Ring.Fin
 import Mathlib.Algebra.Ring.Hom.Basic
 import Mathlib.Algebra.Ring.Hom.Defs
-import Mathlib.Algebra.Ring.Hom.IterateHom
 import Mathlib.Algebra.Ring.Idempotents
 import Mathlib.Algebra.Ring.InjSurj
 import Mathlib.Algebra.Ring.Int

Mathlib/Algebra/Group/Hom/Defs.lean

@@ -6,6 +6,7 @@ Authors: Patrick Massot, Kevin Buzzard, Scott Morrison, Johan Commelin, Chris Hu
 -/
 import Mathlib.Algebra.Group.Pi.Basic
 import Mathlib.Data.FunLike.Basic
+import Mathlib.Logic.Function.Iterate
 
 #align_import algebra.hom.group from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
@@ -1132,29 +1133,31 @@ protected def End := A →+ A
 
 namespace End
 
+instance instFunLike : FunLike (AddMonoid.End A) A A := AddMonoidHom.instFunLike
+instance instAddMonoidHomClass : AddMonoidHomClass (AddMonoid.End A) A A :=
+  AddMonoidHom.instAddMonoidHomClass
+
+instance instOne : One (AddMonoid.End A) where one := .id _
+instance instMul : Mul (AddMonoid.End A) where mul := .comp
+
+@[simp, norm_cast] lemma coe_one : ((1 : AddMonoid.End A) : A → A) = id := rfl
+#align add_monoid.coe_one AddMonoid.End.coe_one
+
+@[simp, norm_cast] lemma coe_mul (f g : AddMonoid.End A) : (f * g : A → A) = f ∘ g := rfl
+#align add_monoid.coe_mul AddMonoid.End.coe_mul
+
 instance monoid : Monoid (AddMonoid.End A) where
-  mul := AddMonoidHom.comp
-  one := AddMonoidHom.id A
   mul_assoc _ _ _ := AddMonoidHom.comp_assoc _ _ _
   mul_one := AddMonoidHom.comp_id
   one_mul := AddMonoidHom.id_comp
+  npow n f := (npowRec n f).copy (Nat.iterate f n) $ by induction n <;> simp [npowRec, *] <;> rfl
+  npow_succ n f := DFunLike.coe_injective $ Function.iterate_succ _ _
 
-instance : Inhabited (AddMonoid.End A) := ⟨1⟩
-
-instance : FunLike (AddMonoid.End A) A A := AddMonoidHom.instFunLike
+@[simp, norm_cast] lemma coe_pow (f : AddMonoid.End A) (n : ℕ) : (↑(f ^ n) : A → A) = f^[n] := rfl
 
-instance : AddMonoidHomClass (AddMonoid.End A) A A := AddMonoidHom.instAddMonoidHomClass
+instance : Inhabited (AddMonoid.End A) := ⟨1⟩
 
 end End
-
-@[simp]
-theorem coe_one : ((1 : AddMonoid.End A) : A → A) = id := rfl
-#align add_monoid.coe_one AddMonoid.coe_one
-
-@[simp]
-theorem coe_mul (f g) : ((f * g : AddMonoid.End A) : A → A) = f ∘ g := rfl
-#align add_monoid.coe_mul AddMonoid.coe_mul
-
 end AddMonoid
 
 end End

Mathlib/Algebra/Ring/Hom/Defs.lean

@@ -681,31 +681,31 @@ theorem id_comp (f : α →+* β) : (id β).comp f = f :=
   ext fun _ => rfl
 #align ring_hom.id_comp RingHom.id_comp
 
-instance : Monoid (α →+* α) where
-  one := id α
-  mul := comp
-  mul_one := comp_id
-  one_mul := id_comp
-  mul_assoc f g h := comp_assoc _ _ _
+instance instOne : One (α →+* α) where one := id _
+instance instMul : Mul (α →+* α) where mul := comp
 
-theorem one_def : (1 : α →+* α) = id α :=
-  rfl
+lemma one_def : (1 : α →+* α) = id α := rfl
 #align ring_hom.one_def RingHom.one_def
 
-theorem mul_def (f g : α →+* α) : f * g = f.comp g :=
-  rfl
+lemma mul_def (f g : α →+* α) : f * g = f.comp g := rfl
 #align ring_hom.mul_def RingHom.mul_def
 
-@[simp]
-theorem coe_one : ⇑(1 : α →+* α) = _root_.id :=
-  rfl
+@[simp, norm_cast] lemma coe_one : ⇑(1 : α →+* α) = _root_.id := rfl
 #align ring_hom.coe_one RingHom.coe_one
 
-@[simp]
-theorem coe_mul (f g : α →+* α) : ⇑(f * g) = f ∘ g :=
-  rfl
+@[simp, norm_cast] lemma coe_mul (f g : α →+* α) : ⇑(f * g) = f ∘ g := rfl
 #align ring_hom.coe_mul RingHom.coe_mul
 
+instance instMonoid : Monoid (α →+* α) where
+  mul_one := comp_id
+  one_mul := id_comp
+  mul_assoc f g h := comp_assoc _ _ _
+  npow n f := (npowRec n f).copy (f^[n]) $ by induction' n <;> simp [npowRec, *]
+  npow_succ n f := DFunLike.coe_injective $ Function.iterate_succ _ _
+
+@[simp, norm_cast] lemma coe_pow (f : α →+* α) (n : ℕ) : ⇑(f ^ n) = f^[n] := rfl
+#align ring_hom.coe_pow RingHom.coe_pow
+
 @[simp]
 theorem cancel_right {g₁ g₂ : β →+* γ} {f : α →+* β} (hf : Surjective f) :
     g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=

Mathlib/Algebra/Ring/Hom/IterateHom.lean

@@ -112,9 +112,7 @@ protected theorem perm_inv (h : IsFixedPt e x) : IsFixedPt (⇑e⁻¹) x :=
   h.equiv_symm
 #align function.is_fixed_pt.perm_inv Function.IsFixedPt.perm_inv
 
-protected theorem perm_pow (h : IsFixedPt e x) (n : ℕ) : IsFixedPt (⇑(e ^ n)) x := by
-  rw [Equiv.Perm.coe_pow]
-  exact h.iterate _
+protected theorem perm_pow (h : IsFixedPt e x) (n : ℕ) : IsFixedPt (⇑(e ^ n)) x := h.iterate _
 #align function.is_fixed_pt.perm_pow Function.IsFixedPt.perm_pow
 
 protected theorem perm_zpow (h : IsFixedPt e x) : ∀ n : ℤ, IsFixedPt (⇑(e ^ n)) x

Mathlib/Dynamics/FixedPoints/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Algebra.Group.TypeTags
 import Mathlib.Algebra.Opposites
 import Mathlib.Logic.Embedding.Basic
+import Mathlib.Logic.Function.Iterate
 
 #align_import group_theory.group_action.defs from "leanprover-community/mathlib"@"dad7ecf9a1feae63e6e49f07619b7087403fb8d4"
 
@@ -1152,6 +1153,8 @@ instance : Monoid (Function.End α) where
   mul_assoc f g h := rfl
   mul_one f := rfl
   one_mul f := rfl
+  npow n f := f^[n]
+  npow_succ n f := Function.iterate_succ _ _
 
 instance : Inhabited (Function.End α) :=
   ⟨1⟩

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -25,14 +25,21 @@ variable {α : Type u} {β : Type v}
 
 namespace Perm
 
+instance instOne : One (Perm α) where one := Equiv.refl _
+instance instMul : Mul (Perm α) where mul f g := Equiv.trans g f
+instance instInv : Inv (Perm α) where inv := Equiv.symm
+instance instPowNat : Pow (Perm α) ℕ where
+  pow f n := ⟨f^[n], f.symm^[n], f.left_inv.iterate _, f.right_inv.iterate _⟩
+
 instance permGroup : Group (Perm α) where
-  mul f g := Equiv.trans g f
-  one := Equiv.refl α
-  inv := Equiv.symm
   mul_assoc f g h := (trans_assoc _ _ _).symm
   one_mul := trans_refl
   mul_one := refl_trans
   mul_left_inv := self_trans_symm
+  npow n f := f ^ n
+  npow_succ n f := coe_fn_injective $ Function.iterate_succ _ _
+  zpow := zpowRec fun n f ↦ f ^ n
+  zpow_succ' n f := coe_fn_injective $ Function.iterate_succ _ _
 #align equiv.perm.perm_group Equiv.Perm.permGroup
 
 @[simp]
@@ -100,11 +107,10 @@ theorem inv_def (f : Perm α) : f⁻¹ = f.symm :=
 @[simp, norm_cast] lemma coe_mul (f g : Perm α) : ⇑(f * g) = f ∘ g := rfl
 #align equiv.perm.coe_mul Equiv.Perm.coe_mul
 
-@[norm_cast] lemma coe_pow (f : Perm α) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
-  hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _
+@[norm_cast] lemma coe_pow (f : Perm α) (n : ℕ) : ⇑(f ^ n) = (f^[n]) := rfl
 #align equiv.perm.coe_pow Equiv.Perm.coe_pow
 
-@[simp] lemma iterate_eq_pow (f : Perm α) (n : ℕ) : f^[n] = ⇑(f ^ n) := (coe_pow _ _).symm
+@[simp] lemma iterate_eq_pow (f : Perm α) (n : ℕ) : (f^[n]) = ⇑(f ^ n) := rfl
 #align equiv.perm.iterate_eq_pow Equiv.Perm.iterate_eq_pow
 
 theorem eq_inv_iff_eq {f : Perm α} {x y : α} : x = f⁻¹ y ↔ f x = y :=