awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ HPow.hPow (α := M) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) (p ^ n) =
    (coeffMonoidHom M p 0 : (a : Perfection M p) → M) f
have rw : HPow.hPow (α := M) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) (p ^ n) =
  HPow.hPow (α := M) ((coeffMonoidHom M p (0 + n) : (a : Perfection M p) → M) f : M) (p ^ n)
Tactic: rw [← coeffMonoidHom_pow_p_pow' _ 0 n, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
rw :
  HPow.hPow (α := M) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) (p ^ n) =
    HPow.hPow (α := M) ((coeffMonoidHom M p (0 + n) : (a : Perfection M p) → M) f : M) (p ^ n)
⊢ HPow.hPow (α := M) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) (p ^ n) =
    (coeffMonoidHom M p 0 : (a : Perfection M p) → M) f
have rw₁ : HPow.hPow (α := M) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) (p ^ n) =
  HPow.hPow (α := M) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) (p ^ n)
Tactic: rw [← coeffMonoidHom_pow_p_pow' _ 0 n, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n m_1 m : ℕ
ih :
  Eq (α := M)
    ((coeffMonoidHom M p (n + m) : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
⊢ Eq (α := M)
    ((coeffMonoidHom M p (n + m.succ) : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m.succ] f) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
have rw : Eq (α := M)
  ((coeffMonoidHom M p (n + m.succ) : (a : Perfection M p) → M)
      ((powMonoidHom p : (a : Perfection M p) → Perfection M p)
          ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
        Perfection M p) :
    M)
  ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
Tactic: rw [Function.iterate_succ_apply', Nat.add_succ, coeffMonoidHom_powMonoidHom, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n m_1 m : ℕ
ih :
  Eq (α := M)
    ((coeffMonoidHom M p (n + m) : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
rw :
  Eq (α := M)
    ((coeffMonoidHom M p (n + m.succ) : (a : Perfection M p) → M)
        ((powMonoidHom p : (a : Perfection M p) → Perfection M p)
            ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
          Perfection M p) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
⊢ Eq (α := M)
    ((coeffMonoidHom M p (n + m.succ) : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m.succ] f) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
have rw₁ : Eq (α := M)
  ((coeffMonoidHom M p (n + m).succ : (a : Perfection M p) → M)
      ((powMonoidHom p : (a : Perfection M p) → Perfection M p)
          ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
        Perfection M p) :
    M)
  ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
Tactic: rw [Function.iterate_succ_apply', Nat.add_succ, coeffMonoidHom_powMonoidHom, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n m_1 m : ℕ
ih :
  Eq (α := M)
    ((coeffMonoidHom M p (n + m) : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
rw :
  Eq (α := M)
    ((coeffMonoidHom M p (n + m.succ) : (a : Perfection M p) → M)
        ((powMonoidHom p : (a : Perfection M p) → Perfection M p)
            ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
          Perfection M p) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
rw₁ :
  Eq (α := M)
    ((coeffMonoidHom M p (n + m).succ : (a : Perfection M p) → M)
        ((powMonoidHom p : (a : Perfection M p) → Perfection M p)
            ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
          Perfection M p) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
rw₂ :
  Eq (α := M)
    ((coeffMonoidHom M p (n + m) : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
⊢ Eq (α := M)
    ((coeffMonoidHom M p (n + m.succ) : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m.succ] f) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
have rw₃ : Eq (α := M) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
  ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
Tactic: rw [Function.iterate_succ_apply', Nat.add_succ, coeffMonoidHom_powMonoidHom, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
hmn : m ≤ n
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
    ((coeffMonoidHom M p (n - m) : (a : Perfection M p) → M) f : M)
have rw : Eq (α := M)
  ((coeffMonoidHom M p n : (a : Perfection M p) → M)
      ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
    M)
  ((coeffMonoidHom M p (n - m + m) : (a : Perfection M p) → M)
      ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
    M)
Tactic: rw [← coeffMonoidHom_iterate_powMonoidHom f (n - m) m, Nat.sub_add_cancel hmn]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
hmn : m ≤ n
rw :
  Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
    ((coeffMonoidHom M p (n - m + m) : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
    ((coeffMonoidHom M p (n - m) : (a : Perfection M p) → M) f : M)
have rw₁ : Eq (α := M)
  ((coeffMonoidHom M p n : (a : Perfection M p) → M)
      ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
    M)
  ((coeffMonoidHom M p n : (a : Perfection M p) → M)
      ((⇑(powMonoidHom p) : (a : Perfection M p) → Perfection M p)^[m] f) :
    M)
Tactic: rw [← coeffMonoidHom_iterate_powMonoidHom f (n - m) m, Nat.sub_add_cancel hmn]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
r : M
n : ℕ
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) (n + 1))
      p =
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n
have rw : Eq.{u_3 + 1} (α := N)
  ((f : (a : M) → N) (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ (n + 1))) : (a : M) → M) r : M) p) : N)
  ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
Tactic: rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
r : M
n : ℕ
rw :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N) (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ (n + 1))) : (a : M) → M) r : M) p) : N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) (n + 1))
      p =
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n
have rw₁ : Eq.{u_3 + 1} (α := N)
  ((f : (a : M) → N)
      (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) (n + 1)).symm : (a : M) → M) r : M) p) :
    N)
  ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
Tactic: rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
r : M
n : ℕ
rw :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N) (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ (n + 1))) : (a : M) → M) r : M) p) : N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₁ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) (n + 1)).symm : (a : M) → M) r : M) p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) (n + 1))
      p =
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n
have rw₂ : Eq.{u_3 + 1} (α := N)
  ((f : (a : M) → N)
      (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n * powMulEquiv M p).symm : (a : M) → M) r : M)
        p) :
    N)
  ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
Tactic: rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
r : M
n : ℕ
rw :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N) (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ (n + 1))) : (a : M) → M) r : M) p) : N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₁ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) (n + 1)).symm : (a : M) → M) r : M) p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₂ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n * powMulEquiv M p).symm : (a : M) → M) r : M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) (n + 1))
      p =
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n
have rw₃ : Eq.{u_3 + 1} (α := N)
  ((f : (a : M) → N)
      (HPow.hPow (α := M)
        (((MulEquiv.trans (powMulEquiv M p) (HPow.hPow (α := M ≃* M) (powMulEquiv M p) n)).symm : (a : M) → M) r : M)
        p) :
    N)
  ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
Tactic: rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
r : M
n : ℕ
rw :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N) (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ (n + 1))) : (a : M) → M) r : M) p) : N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₁ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) (n + 1)).symm : (a : M) → M) r : M) p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₂ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n * powMulEquiv M p).symm : (a : M) → M) r : M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₃ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M)
          (((MulEquiv.trans (powMulEquiv M p) (HPow.hPow (α := M ≃* M) (powMulEquiv M p) n)).symm : (a : M) → M) r : M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) (n + 1))
      p =
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n
have rw₄ : Eq.{u_3 + 1} (α := N)
  ((f : (a : M) → N)
      (HPow.hPow (α := M)
        ((MulEquiv.symm (powMulEquiv M p) : (a : M) → M)
            (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n).symm : (a : M) → M) r : M) :
          M)
        p) :
    N)
  ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
Tactic: rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
r : M
n : ℕ
rw :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N) (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ (n + 1))) : (a : M) → M) r : M) p) : N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₁ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) (n + 1)).symm : (a : M) → M) r : M) p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₂ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n * powMulEquiv M p).symm : (a : M) → M) r : M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₃ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M)
          (((MulEquiv.trans (powMulEquiv M p) (HPow.hPow (α := M ≃* M) (powMulEquiv M p) n)).symm : (a : M) → M) r : M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₄ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M)
          ((MulEquiv.symm (powMulEquiv M p) : (a : M) → M)
              (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n).symm : (a : M) → M) r : M) :
            M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) (n + 1))
      p =
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n
have rw₅ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n).symm : (a : M) → M) r : M) : N)
  ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
Tactic: rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
r : M
n : ℕ
rw :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N) (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ (n + 1))) : (a : M) → M) r : M) p) : N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₁ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) (n + 1)).symm : (a : M) → M) r : M) p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₂ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n * powMulEquiv M p).symm : (a : M) → M) r : M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₃ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M)
          (((MulEquiv.trans (powMulEquiv M p) (HPow.hPow (α := M ≃* M) (powMulEquiv M p) n)).symm : (a : M) → M) r : M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₄ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N)
        (HPow.hPow (α := M)
          ((MulEquiv.symm (powMulEquiv M p) : (a : M) → M)
              (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n).symm : (a : M) → M) r : M) :
            M)
          p) :
      N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
rw₅ :
  Eq.{u_3 + 1} (α := N)
    ((f : (a : M) → N) (((HPow.hPow (α := M ≃* M) (powMulEquiv M p) n).symm : (a : M) → M) r : M) : N)
    ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) (n + 1))
      p =
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n
have rw₆ : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)
  ((fun (n : ℕ) ↦ ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M) : N)) n : N)
Tactic: rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
x : ℕ
⊢ Eq (α := N)
    ((coeffMonoidHom N p x : (a : Perfection N p) → N)
        (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) 1 : M)) ⋯) :
      N)
    ((coeffMonoidHom N p x : (a : Perfection N p) → N) 1 : N)
have simp_rw : Eq.{u_3 + 1} (α := N) ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ x)) : (a : M) → M) 1 : M) : N)
  ((coeffMonoidHom N p x : (a : Perfection N p) → N) 1 : N)
Tactic: simp_rw [coeffMonoidHom_mk, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
x y : M
x_1 : ℕ
⊢ Eq (α := N)
    ((coeffMonoidHom N p x_1 : (a : Perfection N p) → N)
        (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) (x * y) : M)) ⋯) :
      N)
    ((coeffMonoidHom N p x_1 : (a : Perfection N p) → N)
        (HMul.hMul (α := Perfection N p)
          (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) x : M)) ⋯)
          (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) y : M)) ⋯)) :
      N)
have simp_rw : (coeffMonoidHom N p x_1 : (a : Perfection N p) → N)
    (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
      (fun (n : ℕ) ↦
        HMul.hMul (α := N) (β := N)
          ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) x : M) : N)
          ((f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) y : M) : N))
      sorry) =
  HMul.hMul (α := N) (β := N)
    ((coeffMonoidHom N p x_1 : (a : Perfection N p) → N)
        (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) x : M)) sorry) :
      N)
    ((coeffMonoidHom N p x_1 : (a : Perfection N p) → N)
        (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) y : M)) sorry) :
      N)
Tactic: simp_rw [map_mul, coeffMonoidHom_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : M →* N
⊢ MonoidHom.comp (coeffMonoidHom N p 0)
      ((fun (f : M →* N) ↦
          ({
              toFun := fun (r : M) ↦
                Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                  (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
              map_one' := ⋯, map_mul' := ⋯ } :
            MonoidHom.{u_2, u_3} M (Perfection N p)))
        f) =
    f
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := N)
    ((MonoidHom.comp (coeffMonoidHom N p 0)
            ((fun (f : M →* N) ↦
                ({
                    toFun := fun (r : M) ↦
                      Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                        (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                        sorry,
                    map_one' := sorry, map_mul' := sorry } :
                  MonoidHom.{u_2, u_3} M (Perfection N p)))
              f) :
          (a : M) → N)
        x :
      N)
    ((f : (a : M) → N) x : N)
Tactic: ext