awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 : α
simp_rw : (f : (a : α) → α) (a * b) = HMul.hMul (α := α) ((f : (a : α) → α) a : α) b
⊢ f' (a * b) = f' a * b

Tactic:
simp_rw [h, map_mul_right]

Premises used: CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = (⇑f : (a : α) → α)
⊢ (⇑(f.copy f' h) : (a : α) → α) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = (⇑f : (a : α) → α)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Eq (α := (a : α) → α) (⇑(CentroidHom.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Eq (α := α →+ α) (↑(CentroidHom.id α) : α →+ α) (AddMonoidHom.id α)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
⊢ (CentroidHom.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g f : CentroidHom α
⊢ Eq (α := (a : α) → α) (⇑(g.comp f) : (a : α) → α) (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g f : CentroidHom α
a : α
⊢ Eq (α := α) ((g.comp f : (a : α) → α) a : α) ((g : (a : α) → α) ((f : (a : α) → α) a : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g f : CentroidHom α
⊢ Eq (α := α →+ α) (↑(g.comp f) : α →+ α) (AddMonoidHom.comp (↑g : α →+ α) (↑f : α →+ α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
h g f : CentroidHom α
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: CentroidHom.comp, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
⊢ f.comp (CentroidHom.id α) = f

Tactic:
rfl

Premises used: CentroidHom.comp, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
⊢ comp (CentroidHom.id α) f = f

Tactic:
rfl

Premises used: CentroidHom.comp, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
g₁ g₂ f : CentroidHom α
hf : Surjective (α := α) (β := α) (⇑f : (a : α) → α)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h ↦ ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun a ↦ congrFun (congrArg comp a) f⟩

Premises used: Iff.mpr, CentroidHom.ext, Function.Surjective.forall, congrArg, CentroidHom.comp, DFunLike.ext_iff, congrFun, Iff.intro, Iff.mp
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 : α) : α)
rw₂ rw₃ :
  Eq (α := α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((f₁ : (a : α) → α) a : α) : α) ((g : (a : α) → α) ((f₂ : (a : α) → α) a : α) : α)

Tactic:
rw [← comp_apply, h, comp_apply]

Premises used: CentroidHom.comp_apply
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 α
a b : α
⊢ (↑(HAdd.hAdd (α := α →+ α) (↑f : α →+ α) (↑g : α →+ α)) : ZeroHom α α).toFun (a * b) =
    a * (↑(HAdd.hAdd (α := α →+ α) (↑f : α →+ α) (↑g : α →+ α)) : ZeroHom α α).toFun b

Tactic:
simp [map_mul_left, mul_add]

Premises used: CentroidHomClass.map_mul_left, mul_add
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 α
a b : α
⊢ (↑(HAdd.hAdd (α := α →+ α) (↑f : α →+ α) (↑g : α →+ α)) : ZeroHom α α).toFun (a * b) =
    (↑(HAdd.hAdd (α := α →+ α) (↑f : α →+ α) (↑g : α →+ α)) : ZeroHom α α).toFun a * b

Tactic:
simp [map_mul_right, add_mul]

Premises used: add_mul, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 : α
change : HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)
⊢ (↑(HSMul.hSMul (β := α →+ α) n (↑f : α →+ α)) : ZeroHom α α).toFun (a * b) =
    a * (↑(HSMul.hSMul (β := α →+ α) n (↑f : α →+ α)) : ZeroHom α α).toFun b

Tactic:
change n • f (a * b) = a * n • f b

Premises used: HMul.hMul, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 : α)
rw₁ rw₂ : a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)
⊢ HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = a * HSMul.hSMul (β := α) n ((f : (a : α) → α) b : α)

Tactic:
rw [map_mul_left f, ← mul_smul_comm]

Premises used: CentroidHomClass.map_mul_left, mul_smul_comm
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 : α
change : HSMul.hSMul (β := α) n ((f : (a : α) → α) (a * b) : α) = HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α) * b
⊢ (↑(HSMul.hSMul (β := α →+ α) n (↑f : α →+ α)) : ZeroHom α α).toFun (a * b) =
    (↑(HSMul.hSMul (β := α →+ α) n (↑f : α →+ α)) : ZeroHom α α).toFun a * b

Tactic:
change n • f (a * b) = n • f a * b

Premises used: HMul.hMul, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.CentroidHom
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
rw₁ rw₂ : HSMul.hSMul (β := α) n ((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

Tactic:
rw [map_mul_right f, ← smul_mul_assoc]

Premises used: smul_mul_assoc, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 : α
__AddMonoidHom : α →+ α := HPow.hPow (β := ℕ) f.toEnd 0
⊢ (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun (a * b) =
    a * (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun b

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
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)
succ : (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun b
⊢ (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun b

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 * f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun b

Tactic:
(congr_arg f.toEnd ih).trans (f.map_mul_left' _ _)

Premises used: CentroidHom.map_mul_left', AddMonoid.End.instFunLike._aux_1, congr_arg, DFunLike.coe, CentroidHom.toEnd, Eq.trans
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 * f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun b

Tactic:
exact (congr_arg f.toEnd ih).trans (f.map_mul_left' _ _)

Premises used: CentroidHom.map_mul_left', congr_arg, DFunLike.coe, CentroidHom.toEnd, Eq.trans
-- Module: Mathlib.Algebra.Ring.CentroidHom
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
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
⊢ (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = a * (↑(f.toEnd ^ n) : 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' _ _)

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 : α
__AddMonoidHom : α →+ α := HPow.hPow (β := ℕ) f.toEnd 0
⊢ (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun (a * b) =
    (↑(HPow.hPow (β := ℕ) f.toEnd 0) : ZeroHom α α).toFun a * b

Tactic:
rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
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)
succ : (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun a * b
⊢ (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd ^ (n + 1)) : ZeroHom α α).toFun a * b

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 * f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun a * b

Tactic:
(congr_arg f.toEnd ih).trans (f.map_mul_right' _ _)

Premises used: AddMonoid.End.instFunLike._aux_1, congr_arg, CentroidHom.map_mul_right', DFunLike.coe, CentroidHom.toEnd, Eq.trans
-- Module: Mathlib.Algebra.Ring.CentroidHom
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 * f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd * f.toEnd ^ n) : ZeroHom α α).toFun a * b

Tactic:
exact (congr_arg f.toEnd ih).trans (f.map_mul_right' _ _)

Premises used: congr_arg, CentroidHom.map_mul_right', DFunLike.coe, CentroidHom.toEnd, Eq.trans
-- Module: Mathlib.Algebra.Ring.CentroidHom
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
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
⊢ (↑(f.toEnd ^ n) : ZeroHom α α).toFun (a * b) = (↑(f.toEnd ^ n) : 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' _ _)

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Eq.{u_5 + 1} (α := (a : α) → α) (⇑0 : (a : α) → α) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Eq.{u_5 + 1} (α := (a : α) → α) (⇑1 : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f g : CentroidHom α
⊢ (⇑(f + g) : (a : α) → α) = HAdd.hAdd (α := (a : α) → α) (⇑f : (a : α) → α) (⇑g : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f g : CentroidHom α
⊢ Eq (α := (a : α) → α) (⇑(f * g) : (a : α) → α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
M : Type u_2
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : DistribMulAction M α
inst_3 : SMulCommClass M α α
inst_4 : IsScalarTower M α α
n : M
f : CentroidHom α
⊢ (⇑(n • f) : (a : α) → α) = HSMul.hSMul (β := (a : α) → α) n (⇑f : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
⊢ Eq (α := α) ((0 : (a : α) → α) a : α) (0 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
⊢ (1 : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f g : CentroidHom α
a : α
⊢ (f + g : (a : α) → α) a = HAdd.hAdd (α := α) (β := α) ((f : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f g : CentroidHom α
a : α
⊢ Eq (α := α) ((f * g : (a : α) → α) a : α) ((f : (a : α) → α) ((g : (a : α) → α) a : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
M : Type u_2
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : DistribMulAction M α
inst_3 : SMulCommClass M α α
inst_4 : IsScalarTower M α α
n : M
f : CentroidHom α
a : α
⊢ (n • f : (a : α) → α) a = HSMul.hSMul (β := α) n ((f : (a : α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Eq.{u_5 + 1} (α := AddMonoid.End α) (toEnd 0) 0

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
x y : CentroidHom α
⊢ (x + y).toEnd = x.toEnd + y.toEnd

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
M : Type u_2
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : DistribMulAction M α
inst_3 : SMulCommClass M α α
inst_4 : IsScalarTower M α α
m : M
x : CentroidHom α
⊢ (m • x).toEnd = m • x.toEnd

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
n : ℕ
⊢ (⇑(↑n : CentroidHom α) : (a : α) → α) = HSMul.hSMul (β := (a : α) → α) n (⇑(CentroidHom.id α) : (a : α) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
n : ℕ
m : α
⊢ ((↑n : CentroidHom α) : (a : α) → α) m = n • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
⊢ Eq.{u_5 + 1} (α := AddMonoid.End α) (toEnd 1) 1

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
x y : CentroidHom α
⊢ (x * y).toEnd = x.toEnd * y.toEnd

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
x : CentroidHom α
n : ℕ
⊢ (x ^ n).toEnd = x.toEnd ^ n

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, AddMonoidHom.copy, ZeroHom.copy, CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
n : ℕ
⊢ Eq.{u_5 + 1} (α := AddMonoid.End α) (toEnd (↑n : CentroidHom α)) (↑n : AddMonoid.End α)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, CentroidHom.toEnd, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
simp :
  Eq (α := α) ((T : (a : α) → α) ((S : (a : α) → α) (a * b) : α) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
⊢ Eq (α := α) (Function.comp (β := α) (⇑T : (a : α) → α) (⇑S : (a : α) → α) (a * b))
    (Function.comp (β := α) (⇑S : (a : α) → α) (⇑T : (a : α) → α) (a * b))

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Algebra.Ring.CentroidHom
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) : α)
rw₂ :
  Eq (α := α) ((S : (a : α) → α) (HMul.hMul (β := α) a ((T : (a : α) → α) b : α)) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
rw₃ rw₄ :
  Eq (α := α) ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)
⊢ Eq (α := α) ((T : (a : α) → α) ((S : (a : α) → α) (a * b) : α) : α)
    ((S : (a : α) → α) ((T : (a : α) → α) (a * b) : α) : α)

Tactic:
rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]

Premises used: CentroidHomClass.map_mul_left, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : CentroidHom α
a : α
⊢ T • a = (T : (a : α) → α) a

Tactic:
rfl

Premises used: rfl