awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
rw : -(x * x_1 * a) = x * (x_1 * -a)
rw₁ : -(x * (x_1 * a)) = x * (x_1 * -a)
⊢ x * x_1 * -a = x * (x_1 * -a)
have rw₂ : -(x * (x_1 * a)) = x * -(x_1 * a)
Tactic: rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Center (goal)
Goal:
M : Type u_1
inst : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x x_1 : M
rw : -(x * x_1 * a) = x * (x_1 * -a)
rw₁ : -(x * (x_1 * a)) = x * (x_1 * -a)
rw₂ : -(x * (x_1 * a)) = x * -(x_1 * a)
⊢ x * x_1 * -a = x * (x_1 * -a)
have rw₃ : -(x * (x_1 * a)) = -(x * (x_1 * a))
Tactic: rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Centralizer (goal)
Goal:
M : Type u_1
S : Set M
a b : M
inst : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * (a + b) = (a + b) * c
have rw : c * (a + b) = a * c + b * c
Tactic: rw [add_mul, mul_add, ha c hc, hb c hc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Centralizer (goal)
Goal:
M : Type u_1
S : Set M
a b : M
inst : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
rw : c * (a + b) = a * c + b * c
⊢ c * (a + b) = (a + b) * c
have rw₁ : c * a + c * b = a * c + b * c
Tactic: rw [add_mul, mul_add, ha c hc, hb c hc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Centralizer (goal)
Goal:
M : Type u_1
S : Set M
a b : M
inst : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
⊢ c * (a + b) = (a + b) * c
have rw₂ : a * c + c * b = a * c + b * c
Tactic: rw [add_mul, mul_add, ha c hc, hb c hc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Centralizer (goal)
Goal:
M : Type u_1
S : Set M
a b : M
inst : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
rw₂ : a * c + c * b = a * c + b * c
⊢ c * (a + b) = (a + b) * c
have rw₃ : a * c + b * c = a * c + b * c
Tactic: rw [add_mul, mul_add, ha c hc, hb c hc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Centralizer (goal)
Goal:
M : Type u_1
S : Set M
a : M
inst : Mul M
inst_1 : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * -a = -a * c
have rw : -(c * a) = -a * c
Tactic: rw [mul_neg, ha c hc, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Centralizer (goal)
Goal:
M : Type u_1
S : Set M
a : M
inst : Mul M
inst_1 : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
rw : -(c * a) = -a * c
⊢ c * -a = -a * c
have rw₁ : -(a * c) = -a * c
Tactic: rw [mul_neg, ha c hc, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Centralizer (goal)
Goal:
M : Type u_1
S : Set M
a : M
inst : Mul M
inst_1 : HasDistribNeg M
ha : a ∈ S.centralizer
c : M
hc : c ∈ S
rw : -(c * a) = -a * c
rw₁ : -(a * c) = -a * c
⊢ c * -a = -a * c
have rw₂ : -(a * c) = -(a * c)
Tactic: rw [mul_neg, ha c hc, neg_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f g : CentroidHom α
h :
  Eq.{u_5 + 1} (α := (a : α) → α) ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun) f)
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun) g)
⊢ f = g
have mk : ∀ (toAddMonoidHom : α →+ α)
  (map_mul_left' :
    ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom : ZeroHom α α).toFun b)
  (map_mul_right' :
    ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom : ZeroHom α α).toFun a * b)
  (h :
    Eq.{u_5 + 1} (α := (a : α) → α)
      ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
        { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
      ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun) g)),
  { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' :
      CentroidHom α } =
    g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g : CentroidHom α
toAddMonoidHom : α →+ α
map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom : ZeroHom α α).toFun b
map_mul_right' :
  ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom : ZeroHom α α).toFun a * b
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun) g)
⊢ { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' :
      CentroidHom α } =
    g
have mk : ∀ (toAddMonoidHom_1 : α →+ α)
  (map_mul_left'_1 :
    ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom_1 : ZeroHom α α).toFun b)
  (map_mul_right'_1 :
    ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom_1 : ZeroHom α α).toFun a * b)
  (h :
    Eq.{u_5 + 1} (α := (a : α) → α)
      ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
        { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
      ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
        { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 })),
  { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' :
      CentroidHom α } =
    { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
toAddMonoidHom : α →+ α
map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom : ZeroHom α α).toFun b
map_mul_right' :
  ∀ (a b : α), (↑toAddMonoidHom : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom : ZeroHom α α).toFun a * b
toAddMonoidHom_1 : α →+ α
map_mul_left'_1 :
  ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = a * (↑toAddMonoidHom_1 : ZeroHom α α).toFun b
map_mul_right'_1 :
  ∀ (a b : α), (↑toAddMonoidHom_1 : ZeroHom α α).toFun (a * b) = (↑toAddMonoidHom_1 : ZeroHom α α).toFun a * b
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' })
    ((fun (f : CentroidHom α) ↦ (↑f.toAddMonoidHom : ZeroHom α α).toFun)
      { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 })
⊢ { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' :
      CentroidHom α } =
    { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 }
have mk : ∀ (x : α), Eq (α := α) ((toAddMonoidHom : (a : α) → α) x : α) ((toAddMonoidHom_1 : (a : α) → α) x : α)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = (⇑f : (a : α) → α)
a b : α
⊢ f' (a * b) = a * f' b
have simp_rw : (f : (a : α) → α) (a * b) = HMul.hMul (β := α) a ((f : (a : α) → α) b : α)
Tactic: simp_rw [h, map_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = (⇑f : (a : α) → α)
a b : α
⊢ f' (a * b) = f' a * b
have simp_rw : (f : (a : α) → α) (a * b) = HMul.hMul (α := α) ((f : (a : α) → α) a : α) b
Tactic: simp_rw [h, map_mul_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective (α := α) (β := α) (⇑g : (a : α) → α)
h : g.comp f₁ = g.comp f₂
a : α
⊢ Eq (α := α) ((g : (a : α) → α) ((f₁ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
have rw : Eq (α := α) ((g.comp f₁ : (a : α) → α) a : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective (α := α) (β := α) (⇑g : (a : α) → α)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq (α := α) ((g.comp f₁ : (a : α) → α) a : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((f₁ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
have rw₁ : Eq (α := α) ((g.comp f₂ : (a : α) → α) a : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective (α := α) (β := α) (⇑g : (a : α) → α)
h : g.comp f₁ = g.comp f₂
a : α
rw : Eq (α := α) ((g.comp f₁ : (a : α) → α) a : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
rw₁ : Eq (α := α) ((g.comp f₂ : (a : α) → α) a : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((f₁ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
have rw₂ : Eq (α := α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
⊢ (↑(HSMul.hSMul (β := α →+ α) n (↑f : α →+ α)) : ZeroHom α α).toFun (a * b) =
    a * (↑(HSMul.hSMul (β := α →+ α) n (↑f : α →+ α)) : ZeroHom α α).toFun b
have change : HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)
Tactic: change n • f (a * b) = a * n • f b
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
⊢ HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)
have rw : n • HMul.hMul (β := α) a ((f : (a : α) → α) b : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)
Tactic: rw [map_mul_left f, ← mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
rw : n • HMul.hMul (β := α) a ((f : (a : α) → α) b : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)
⊢ HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)
have rw₁ : a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)
Tactic: rw [map_mul_left f, ← mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
⊢ (↑(HSMul.hSMul (β := α →+ α) n (↑f : α →+ α)) : ZeroHom α α).toFun (a * b) =
    (↑(HSMul.hSMul (β := α →+ α) n (↑f : α →+ α)) : ZeroHom α α).toFun a * b
have change : HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α) * b
Tactic: change n • f (a * b) = n • f a * b
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
⊢ HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α) * b
have rw : n • HMul.hMul (α := α) ((f : (a : α) → α) a : α) b = HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α) * b
Tactic: rw [map_mul_right f, ← smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
rw : n • HMul.hMul (α := α) ((f : (a : α) → α) a : α) b = HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α) * b
⊢ HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α) * b
have rw₁ : HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α) * b = HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α) * b
Tactic: rw [map_mul_right f, ← smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
f : CentroidHom α
a b : α
n : ℕ
ih :
  let __AddMonoidHom := f.toEnd ^ n;
  (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd ^ n) : ZeroHom α α).toFun b
__AddMonoidHom : α →+ α := f.toEnd ^ (n + 1)
⊢ (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun b
have succ : (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun b
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
f : CentroidHom α
n : ℕ
a b : α
⊢ (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd ^ n) : ZeroHom α α).toFun b
have zero : (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun (a * b) =
  a * (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun b
Tactic: induction n with
        | zero => rfl
        | succ n ih =>
          rw [pow_succ']
          exact (congr_arg f.toEnd ih).trans (f.map_mul_left' _ _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
f : CentroidHom α
n : ℕ
a b : α
zero :
  (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun (a * b) =
    a * (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun b
⊢ (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd ^ n) : ZeroHom α α).toFun b
have succ : ∀ (n : ℕ)
  (ih :
    let __AddMonoidHom := f.toEnd ^ n;
    (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd ^ n) : ZeroHom α α).toFun b),
  (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun b
Tactic: induction n with
        | zero => rfl
        | succ n ih =>
          rw [pow_succ']
          exact (congr_arg f.toEnd ih).trans (f.map_mul_left' _ _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
f : CentroidHom α
a b : α
n : ℕ
ih :
  let __AddMonoidHom := f.toEnd ^ n;
  (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd ^ n) : ZeroHom α α).toFun a * b
__AddMonoidHom : α →+ α := f.toEnd ^ (n + 1)
⊢ (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun a * b
have succ : (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun a * b
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
f : CentroidHom α
n : ℕ
a b : α
⊢ (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd ^ n) : ZeroHom α α).toFun a * b
have zero : (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun (a * b) =
  (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun a * b
Tactic: induction n with
        | zero => rfl
        | succ n ih =>
          rw [pow_succ']
          exact (congr_arg f.toEnd ih).trans (f.map_mul_right' _ _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R
inst_4 : DistribMulAction M α
inst_5 : SMulCommClass M α α
inst_6 : IsScalarTower M α α
inst_7 : DistribMulAction N α
inst_8 : SMulCommClass N α α
inst_9 : IsScalarTower N α α
inst_10 : Module R α
inst_11 : SMulCommClass R α α
inst_12 : IsScalarTower R α α
f : CentroidHom α
n : ℕ
a b : α
zero :
  (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun (a * b) =
    (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun a * b
⊢ (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd ^ n) : ZeroHom α α).toFun a * b
have succ : ∀ (n : ℕ)
  (ih :
    let __AddMonoidHom := f.toEnd ^ n;
    (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd ^ n) : ZeroHom α α).toFun a * b),
  (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun a * b
Tactic: induction n with
        | zero => rfl
        | succ n ih =>
          rw [pow_succ']
          exact (congr_arg f.toEnd ih).trans (f.map_mul_right' _ _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ Eq (α := α) (Function.comp (β := α) (⇑T : (a : α) → α) (⇑S : (a : α) → α) (a * b))
    (Function.comp (β := α) (⇑S : (a : α) → α) (⇑T : (a : α) → α) (a * b))
have simp : Eq (α := α) ((T : (a : α) → α) ((S : (a : α) → α) (a * b) : α) : α)
  ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
Tactic: simp only [Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ Eq (α := α) ((T : (a : α) → α) ((S : (a : α) → α) (a * b) : α) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
have rw : Eq (α := α) ((T : (a : α) → α) (HMul.hMul (α := α) ((S : (a : α) → α) a : α) b) : α)
  ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
Tactic: rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
rw :
  Eq (α := α) ((T : (a : α) → α) (HMul.hMul (α := α) ((S : (a : α) → α) a : α) b) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
⊢ Eq (α := α) ((T : (a : α) → α) ((S : (a : α) → α) (a * b) : α) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
have rw₁ : HMul.hMul (α := α) (β := α) ((S : (a : α) → α) a : α) ((T : (a : α) → α) b : α) =
  (S : (a : α) → α) ((T : (a : α) → α) (a * b) : α)
Tactic: rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
rw :
  Eq (α := α) ((T : (a : α) → α) (HMul.hMul (α := α) ((S : (a : α) → α) a : α) b) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
rw₁ :
  HMul.hMul (α := α) (β := α) ((S : (a : α) → α) a : α) ((T : (a : α) → α) b : α) =
    (S : (a : α) → α) ((T : (a : α) → α) (a * b) : α)
⊢ Eq (α := α) ((T : (a : α) → α) ((S : (a : α) → α) (a * b) : α) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
have rw₂ : Eq (α := α) ((S : (a : α) → α) (HMul.hMul (β := α) a ((T : (a : α) → α) b : α)) : α)
  ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
Tactic: rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]