awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
⊢ HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
        HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) : T) ((f : (a : R) → T) r₁ : T) +
      HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
have c : HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
    HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
⊢ HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T) *
      HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
have c : HMul.hMul (β := T)
    (HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
      ((f : (a : R) → T) r₃ : T))
    ((f : (a : R) → T) r₂ : T) =
  HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑s₃ : R) * (↑s₁ : R) = r₃ * (↑s₂ : R)
⊢ HMul.hMul (β := T)
      (HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
        ((f : (a : R) → T) r₃ : T))
      ((f : (a : R) → T) r₂ : T) =
    HMul.hMul (α := T) (β := T) ((↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T) : T) ((f : (a : R) → T) r₂ : T)
have c : HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
    ((f : (a : R) → T) r₃ : T) =
  (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑(s₃ * s₁) : R) = r₃ * (↑s₂ : R)
⊢ HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
      ((f : (a : R) → T) r₃ : T) =
    (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)
have h₃' : s₃ * s₁ = Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) sorry
Tactic: have h₃' := Subtype.coe_eq_of_eq_mk h₃
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑(s₃ * s₁) : R) = r₃ * (↑s₂ : R)
h₃' : s₃ * s₁ = Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯
⊢ HMul.hMul (β := T) (HMul.hMul (α := T) (↑((fS : (a : ↥S) → Tˣ) s₁)⁻¹ : T) (↑((fS : (a : ↥S) → Tˣ) s₃)⁻¹ : T))
      ((f : (a : R) → T) r₃ : T) =
    (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)
have c : HMul.hMul (α := T) (β := T)
    ((↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) sorry))⁻¹ : T) : T)
    ((f : (a : R) → T) r₃ : T) =
  (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)
Tactic: rw [← Units.val_mul, ← mul_inv_rev, ← fS.map_mul, h₃']
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : AddCommMonoid X
inst_3 : Module R X
T : Type u_3
inst_4 : Semiring T
f : R →+* T
fS : MonoidHom.{u_1, u_3} (↥S) Tˣ
hf : ∀ (s : ↥S), Eq.{u_3 + 1} (α := T) ((f : (a : R) → T) (↑s : R) : T) ((↑((fS : (a : ↥S) → Tˣ) s) : T) : T)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : (↑(s₃ * s₁) : R) = r₃ * (↑s₂ : R)
h₃' : s₃ * s₁ = Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯
⊢ HMul.hMul (α := T) (β := T)
      ((↑((fS : (a : ↥S) → Tˣ) (Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) ⋯))⁻¹ : T) : T)
      ((f : (a : R) → T) r₃ : T) =
    (↑((fS : (a : ↥S) → Tˣ) s₂)⁻¹ : T)
have c : HMul.hMul (α := T) (β := T) ((f : (a : R) → T) r₃ : T) ((f : (a : R) → T) (↑s₂ : R) : T) =
  (f : (a : R) → T) (↑(Subtype.mk (p := fun (a : R) ↦ a ∈ S) (r₃ * (↑s₂ : R)) sorry) : R)
Tactic: rw [Units.inv_mul_eq_iff_eq_mul, Units.eq_mul_inv_iff_mul_eq, ← hf, ← hf]
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
h :
  Eq (α := OreLocalization S R) ((numeratorHom : (a : R) → OreLocalization S R) r₁ : OreLocalization S R)
    ((numeratorHom : (a : R) → OreLocalization S R) r₂ : OreLocalization S R)
⊢ r₁ = r₂
have h₁ : ∃ (u : ↥S) (v : R), u • r₂ = v • r₁ ∧ (↑u : R) * (↑1 : R) = v * (↑1 : R)
Tactic: rw [numeratorHom_apply, numeratorHom_apply, oreDiv_eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (goal)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
h : ∃ (u : ↥S) (v : R), u • r₂ = v • r₁ ∧ (↑u : R) * (↑1 : R) = v * (↑1 : R)
⊢ r₁ = r₂
have rcases : ∀ (u : ↥S) (v : R) (h₁ : u • r₂ = v • r₁) (h₂ : (↑u : R) * (↑1 : R) = v * (↑1 : R)), r₁ = r₂
Tactic: rcases h with ⟨u, v, h₁, h₂⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : u • r₂ = v • r₁
h₂ : (↑u : R) * (↑1 : R) = v * (↑1 : R)
⊢ r₁ = r₂
have h₃ : (↑u : R) = v
Tactic: simp only [S.coe_one, mul_one, Submonoid.smul_def, smul_eq_mul] at h₁ h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.OreLocalization.Ring (hypothesis)
Goal:
R : Type u_1
inst : Ring R
S : Submonoid R
inst_1 : OreSet S
hS : S ≤ nonZeroDivisorsLeft R
r₁ r₂ : R
u : ↥S
v : R
h₁ : (↑u : R) * r₂ = v * r₁
h₂ : (↑u : R) = v
⊢ r₁ = r₂
have h₃ : (↑u : R) * (r₂ - r₁) = 0
Tactic: rw [← h₂, ← sub_eq_zero, ← mul_sub] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.OrzechProperty (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
⊢ Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
have obtain : ∀ (n : ℕ) (g : (Fin n → R) →ₗ[R] M)
  (hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)),
  Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
Tactic: obtain ⟨n, g, hg⟩ := Module.Finite.exists_fin' R M
-- Lean 4 proof step from Mathlib.RingTheory.OrzechProperty (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
⊢ Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
have this : Small.{u, v} M
Tactic: haveI := small_of_surjective hg
-- Lean 4 proof step from Mathlib.RingTheory.OrzechProperty (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
⊢ Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
have this₁ : Module.Finite R (Shrink.{u, v} M)
Tactic: haveI := Module.Finite.equiv j.symm
-- Lean 4 proof step from Mathlib.RingTheory.OrzechProperty (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hi : Injective.{w + 1, v + 1} (α := N) (β := M) (⇑i : (a : N) → M)
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this_3 : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ i
⊢ Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
have hi₁ : Injective.{w + 1, u + 1} (α := N) (β := Shrink.{u, v} M) (⇑i' : (a : N) → Shrink.{u, v} M)
Tactic: replace hi : Injective i' := by simpa [i'] using hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.OrzechProperty (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : OrzechProperty R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module.Finite R M
N : Type w
inst_5 : AddCommMonoid N
inst_6 : Module R N
i f : N →ₗ[R] M
hf : Surjective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
n : ℕ
g : (Fin n → R) →ₗ[R] M
hg : Surjective.{u + 1, v + 1} (α := Fin n → R) (β := M) (⇑g : (a : Fin n → R) → M)
this_1 : Small.{u, v} M
this_2 : AddCommMonoid (Shrink.{u, v} M) := Equiv.addCommMonoid (Equiv.symm (equivShrink M))
this_3 : Module R (Shrink.{u, v} M) := Equiv.module R (Equiv.symm (equivShrink M))
j : Shrink.{u, v} M ≃ₗ[R] M := Equiv.linearEquiv R (Equiv.symm (equivShrink M))
this : Module.Finite R (Shrink.{u, v} M)
i' : N →ₗ[R] Shrink.{u, v} M := (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ i
hi : Injective.{w + 1, u + 1} (α := N) (β := Shrink.{u, v} M) (⇑i' : (a : N) → Shrink.{u, v} M)
f' : ↥i'.range →ₗ[R] Shrink.{u, v} M :=
  (↑j.symm : M →ₗ[R] Shrink.{u, v} M) ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (LinearEquiv.ofInjective i' hi)) : ↥i'.range →ₗ[R] N)
⊢ Injective.{w + 1, v + 1} (α := N) (β := M) (⇑f : (a : N) → M)
have hf₁ : Surjective (α := ↥i'.range) (β := Shrink.{u, v} M) (⇑f' : (a : ↥i'.range) → Shrink.{u, v} M)
Tactic: replace hf : Surjective f' := by simpa [f'] using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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) (f ^ p) : M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M)
have rw : HPow.hPow (α := M) ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M) p =
  (coeffMonoidHom M p n : (a : Perfection M p) → M) f
Tactic: rw [map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) ((fun (x : Perfection M p) ↦ x ^ p) x) = x
have h : ∀ (n : ℕ),
  Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) ((fun (x : Perfection M p) ↦ x ^ p) x)) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (fun (x : Perfection M p) ↦ x ^ p) ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x) = x
have h : ∀ (n : ℕ),
  Eq (α := M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M)
        ((fun (x : Perfection M p) ↦ x ^ p) ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x)) :
      M)
    ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (powMulEquiv (Perfection M p) p : (a : Perfection M p) → Perfection M p)
      ((pthRootMonoidHom M p : (a : Perfection M p) → Perfection M p) x) =
    x
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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) f : Perfection M p) :
      M)
    ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M)
have 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)
Tactic: rw [← coe_pthRootMonoidHom_eq_powMulEquiv_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : (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)
have 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)
Tactic: rw [Function.iterate_succ_apply', coeffMonoidHom_symm_powMulEquiv, 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 : ℕ
⊢ 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)
have 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)
Tactic: induction m generalizing n with
  | zero => rfl
  | succ m ih =>
    rw [Function.iterate_succ_apply', coeffMonoidHom_symm_powMulEquiv, ih]
    grind
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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)
have 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)
Tactic: induction m generalizing n with
  | zero => rfl
  | succ m ih =>
    rw [Function.iterate_succ_apply', coeffMonoidHom_symm_powMulEquiv, ih]
    grind
Cleared hypotheses: n, m
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ, pow_mul, Nat.add_succ, coeffMonoidHom_pow_p, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ, pow_mul, Nat.add_succ, coeffMonoidHom_pow_p, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ, pow_mul, Nat.add_succ, coeffMonoidHom_pow_p, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ, pow_mul, Nat.add_succ, coeffMonoidHom_pow_p, ih]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M : Type u_1
inst : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ 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
have 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)
Tactic: rw [← map_pow, coeffMonoidHom_pow_p_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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
have 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)
Tactic: rw [← map_pow, coeffMonoidHom_pow_p_pow]