awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
h :
  ∀ (n : ℕ),
    Eq (α := M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M)
          ((powMulEquiv (Perfection M p) p : (a : Perfection M p) → Perfection M p)
              ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x) :
            Perfection M p) :
        M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)
⊢ (powMulEquiv (Perfection M p) p : (a : Perfection M p) → Perfection M p)
      ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x) =
    x

Tactic:
ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
n : ℕ
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((powMulEquiv (Perfection M p) p : (a : Perfection M p) → Perfection M p)
            ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x) :
          Perfection M p) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
⊢ Eq (α := (a : Perfection M p) → Perfection M p) (⇑(pthRootMonoidHom M p) : (a : Perfection M p) → Perfection M p)
    (⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)

Tactic:
congr($pthRootMonoidHom_eq_powMulEquiv_symm)

Premises used: Perfection.pthRootMonoidHom_eq_powMulEquiv_symm, congrArg, id, DFunLike.coe
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
rw :
  Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) f : Perfection M p) :
      M)
    ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M)
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((MulEquiv.symm (powMulEquiv (Perfection M p) p) : (a : Perfection M p) → Perfection M p) f : Perfection M p) :
      M)
    ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M)

Tactic:
rw [← coe_pthRootMonoidHom_eq_powMulEquiv_symm]

Premises used: Perfection.coe_pthRootMonoidHom_eq_powMulEquiv_symm
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) f : Perfection M p) :
      M)
    ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)^[0] f) :
      M)
    ((coeffMonoidHom M p (n + 0) : (a : Perfection M p) → M) f : M)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
m : ℕ
ih :
  ∀ (n : ℕ),
    Eq (α := M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M)
          ((⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)^[m] f) :
        M)
      ((coeffMonoidHom M p (n + m) : (a : Perfection M p) → M) f : M)
n : ℕ
succ :
  Eq (α := M) ((coeffMonoidHom M p (n + 1 + m) : (a : Perfection M p) → M) f : M)
    ((coeffMonoidHom M p (n + (m + 1)) : (a : Perfection M p) → M) f : M)
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)^[m + 1] f) :
      M)
    ((coeffMonoidHom M p (n + (m + 1)) : (a : Perfection M p) → M) f : M)

Tactic:
rw [Function.iterate_succ_apply', coeffMonoidHom_symm_powMulEquiv, ih]

Premises used: Function.iterate_succ_apply', Perfection.coeffMonoidHom_symm_powMulEquiv
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
m : ℕ
ih :
  ∀ (n : ℕ),
    Eq (α := M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M)
          ((⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)^[m] f) :
        M)
      ((coeffMonoidHom M p (n + m) : (a : Perfection M p) → M) f : M)
n : ℕ
⊢ Eq (α := M) ((coeffMonoidHom M p (n + 1 + m) : (a : Perfection M p) → M) f : M)
    ((coeffMonoidHom M p (n + (m + 1)) : (a : Perfection M p) → M) f : M)

Tactic:
grind
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n m : ℕ
zero :
  ∀ (n : ℕ),
    Eq (α := M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M)
          ((⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)^[0] f) :
        M)
      ((coeffMonoidHom M p (n + 0) : (a : Perfection M p) → M) f : M)
succ :
  ∀ (m : ℕ)
    (ih :
      ∀ (n : ℕ),
        Eq (α := M)
          ((coeffMonoidHom M p n : (a : Perfection M p) → M)
              ((⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)^[m] f) :
            M)
          ((coeffMonoidHom M p (n + m) : (a : Perfection M p) → M) f : M))
    (n : ℕ),
    Eq (α := M)
      ((coeffMonoidHom M p n : (a : Perfection M p) → M)
          ((⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)^[m + 1] f) :
        M)
      ((coeffMonoidHom M p (n + (m + 1)) : (a : Perfection M p) → M) f : M)
⊢ Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((⇑(MulEquiv.symm (powMulEquiv (Perfection M p) p)) : (a : Perfection M p) → Perfection M p)^[m] f) :
      M)
    ((coeffMonoidHom M p (n + m) : (a : Perfection M p) → M) f : M)

Tactic:
induction m generalizing n with
  | zero => rfl
  | succ m ih =>
    rw [Function.iterate_succ_apply', coeffMonoidHom_symm_powMulEquiv, ih]
    grind

Premises used: Function.iterate_succ_apply', Perfection.coeffMonoidHom_symm_powMulEquiv
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ Eq (α := M) ((coeffMonoidHom M p (m + Nat.zero) : (a : Perfection M p) → M) (f ^ p ^ Nat.zero) : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
m n_1 n : ℕ
ih :
  Eq (α := M) ((coeffMonoidHom M p (m + n) : (a : Perfection M p) → M) (f ^ p ^ n) : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
rw :
  Eq (α := M) ((coeffMonoidHom M p (m + n.succ) : (a : Perfection M p) → M) (f ^ (p ^ n * p)) : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
rw₁ :
  Eq (α := M) ((coeffMonoidHom M p (m + n.succ) : (a : Perfection M p) → M) ((f ^ p ^ n) ^ p) : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
rw₂ :
  Eq (α := M) ((coeffMonoidHom M p (m + n).succ : (a : Perfection M p) → M) ((f ^ p ^ n) ^ p) : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
rw₃ :
  Eq (α := M) ((coeffMonoidHom M p (m + n) : (a : Perfection M p) → M) (f ^ p ^ n) : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
rw₄ rw₅ :
  Eq (α := M) ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
⊢ Eq (α := M) ((coeffMonoidHom M p (m + n.succ) : (a : Perfection M p) → M) (f ^ p ^ n.succ) : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)

Tactic:
rw [pow_succ, pow_mul, Nat.add_succ, coeffMonoidHom_pow_p, ih]

Premises used: pow_succ, pow_mul, Nat.add_succ, Perfection.coeffMonoidHom_pow_p
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
rw :
  Eq (α := M) ((coeffMonoidHom M p (m + n) : (a : Perfection M p) → M) (f ^ p ^ n) : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
rw₁ rw₂ :
  Eq (α := M) ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
    ((coeffMonoidHom M p m : (a : Perfection M p) → M) f : M)
⊢ HPow.hPow (α := M) ((coeffMonoidHom M p (m + n) : (a : Perfection M p) → M) f : M) (p ^ n) =
    (coeffMonoidHom M p m : (a : Perfection M p) → M) f

Tactic:
rw [← map_pow, coeffMonoidHom_pow_p_pow]

Premises used: map_pow, Perfection.coeffMonoidHom_pow_p_pow
-- Module: Mathlib.RingTheory.Perfection
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)
rw₁ 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)
⊢ 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

Tactic:
rw [← coeffMonoidHom_pow_p_pow' _ 0 n, zero_add]

Premises used: zero_add, Perfection.coeffMonoidHom_pow_p_pow', OfNat.ofNat
-- Module: Mathlib.RingTheory.Perfection
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
n : ℕ
⊢ Eq (α := M)
    ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M)
        ((powMonoidHom p : (a : Perfection M p) → Perfection M p) f : Perfection M p) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)

Tactic:
coeffMonoidHom_pow_p f n

Premises used: Perfection.coeffMonoidHom_pow_p
-- Module: Mathlib.RingTheory.Perfection
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)
rw₃ 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)
⊢ 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)

Tactic:
rw [Function.iterate_succ_apply', Nat.add_succ, coeffMonoidHom_powMonoidHom, ih]

Premises used: Function.iterate_succ_apply', Perfection.coeffMonoidHom_powMonoidHom, Nat.add_succ
-- Module: Mathlib.RingTheory.Perfection
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← coeffMonoidHom_iterate_powMonoidHom f (n - m) m, Nat.sub_add_cancel hmn]

Premises used: HSub.hSub, Nat.sub_add_cancel, Perfection.coeffMonoidHom_iterate_powMonoidHom
-- Module: Mathlib.RingTheory.Perfection
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)
rw₆ 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)
⊢ 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

Tactic:
rw [← map_pow, powMulEquiv_pow, pow_succ, MulAut.mul_def, MulEquiv.symm_trans_apply,
          powMulEquiv_symm_pow_p, ← powMulEquiv_pow]

Premises used: pow_succ, powMulEquiv_pow, map_pow, MulAut.mul_def, MulEquiv.symm_trans_apply, powMulEquiv_symm_pow_p
-- Module: Mathlib.RingTheory.Perfection
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 : ℕ
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)
⊢ 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)

Tactic:
simp_rw [coeffMonoidHom_mk, map_one]

Premises used: Perfection.coeffMonoidHom_mk, map_one
-- Module: Mathlib.RingTheory.Perfection
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 : ℕ
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))
        ⋯) =
    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)) ⋯) :
        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)) ⋯) :
        N)
⊢ 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)

Tactic:
simp_rw [map_mul, coeffMonoidHom_mk]

Premises used: Perfection.coeffMonoidHom_mk, map_mul
-- Module: Mathlib.RingTheory.Perfection
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
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))
                          ⋯,
                      map_one' := ⋯, map_mul' := ⋯ } :
                    MonoidHom.{u_2, u_3} M (Perfection N p)))
                f) :
            (a : M) → N)
          x :
        N)
      ((f : (a : M) → N) x : 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

Tactic:
ext
-- Module: Mathlib.RingTheory.Perfection
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 : 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))
                        ⋯,
                    map_one' := ⋯, map_mul' := ⋯ } :
                  MonoidHom.{u_2, u_3} M (Perfection N p)))
              f) :
          (a : M) → N)
        x :
      N)
    ((f : (a : M) → N) x : N)

Tactic:
simp
-- Module: Mathlib.RingTheory.Perfection
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 : MonoidHom.{u_2, u_3} M (Perfection N p)
h :
  ∀ (m : M) (n : ℕ),
    Eq (α := N)
      ((coeffMonoidHom N p n : (a : Perfection N p) → N)
          ((((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)))
                    (MonoidHom.comp (coeffMonoidHom N p 0) f) :
                  MonoidHom.{u_2, u_3} M (Perfection N p)) :
                (a : M) → Perfection N p)
              m :
            Perfection N p) :
        N)
      ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
⊢ (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)))
      (MonoidHom.comp (coeffMonoidHom N p 0) f) =
    f

Tactic:
ext m n
-- Module: Mathlib.RingTheory.Perfection
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 : MonoidHom.{u_2, u_3} M (Perfection N p)
m : M
n : ℕ
h :
  Eq (α := N)
    ((coeffMonoidHom N p 0 : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
⊢ Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        ((((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)))
                  (MonoidHom.comp (coeffMonoidHom N p 0) f) :
                MonoidHom.{u_2, u_3} M (Perfection N p)) :
              (a : M) → Perfection N p)
            m :
          Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)

Tactic:
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk,
      coeffMonoidHom_mk]

Premises used: MonoidHom.coe_comp, OneHom.coe_mk, Perfection.coeffMonoidHom_mk, MonoidHom.coe_mk, Function.comp_apply