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 α
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 α α
⊢ SMulCommClass α (CentroidHom α) α

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
h :
  ∀ (T : AddMonoid.End α),
    Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T ↔
      Membership.mem (γ := Subsemiring (AddMonoid.End α))
        (Subsemiring.centralizer
          (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
        T
⊢ Eq (α := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
    (Subsemiring.centralizer
      (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))

Tactic:
ext T
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T ↔
    Membership.mem (γ := Subsemiring (AddMonoid.End α))
      (Subsemiring.centralizer
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
      T

Tactic:
⟨?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T →
    Membership.mem (γ := Subsemiring (AddMonoid.End α))
      (Subsemiring.centralizer
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
      T
h₁ :
  ∀
    (h :
      Membership.mem (γ := Subsemiring (AddMonoid.End α))
        (Subsemiring.centralizer
          (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
        T),
    Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T ↔
    Membership.mem (γ := Subsemiring (AddMonoid.End α))
      (Subsemiring.centralizer
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
      T

Tactic:
refine ⟨?_, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
a : α
⊢ HMul.hMul (α := AddMonoid.End α) (β := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
      ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) f : AddMonoid.End α) =
    HMul.hMul (α := AddMonoid.End α) (β := AddMonoid.End α)
      ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) f : AddMonoid.End α)
      ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)

Tactic:
AddMonoidHom.ext fun b ↦ (map_mul_left f a b).symm

Premises used: CentroidHomClass.map_mul_left, AddMonoidHom.ext, AddMonoid.End, Eq.symm
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
a : α
⊢ HMul.hMul (α := AddMonoid.End α) (β := AddMonoid.End α) ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
      ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) f : AddMonoid.End α) =
    HMul.hMul (α := AddMonoid.End α) (β := AddMonoid.End α)
      ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) f : AddMonoid.End α)
      ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)

Tactic:
exact AddMonoidHom.ext fun b ↦ (map_mul_left f a b).symm

Premises used: AddMonoidHom.ext
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ HMul.hMul (α := AddMonoid.End α) (β := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) b : AddMonoid.End α)
      ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) f : AddMonoid.End α) =
    HMul.hMul (α := AddMonoid.End α) (β := AddMonoid.End α)
      ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) f : AddMonoid.End α)
      ((R : (a : α) → AddMonoid.End α) b : AddMonoid.End α)

Tactic:
AddMonoidHom.ext fun a ↦ (map_mul_right f a b).symm

Premises used: AddMonoidHom.ext, AddMonoid.End, Eq.symm, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
f : CentroidHom α
b : α
⊢ HMul.hMul (α := AddMonoid.End α) (β := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) b : AddMonoid.End α)
      ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) f : AddMonoid.End α) =
    HMul.hMul (α := AddMonoid.End α) (β := AddMonoid.End α)
      ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) f : AddMonoid.End α)
      ((R : (a : α) → AddMonoid.End α) b : AddMonoid.End α)

Tactic:
exact AddMonoidHom.ext fun a ↦ (map_mul_right f a b).symm

Premises used: AddMonoidHom.ext
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  Membership.mem (γ := Subsemiring (AddMonoid.End α))
    (Subsemiring.centralizer
      (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)))
    T
⊢ ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g

Tactic:
rw [Subsemiring.mem_centralizer_iff] at h

Premises used: Subsemiring.mem_centralizer_iff
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T

Tactic:
⟨⟨T, fun a b ↦ ?_, fun a b ↦ ?_⟩, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, CentroidHom.mk, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g
h₁ : ∀ (a b : α), (↑T : ZeroHom α α).toFun (a * b) = a * (↑T : ZeroHom α α).toFun b
h₂ : ∀ (a b : α), (↑T : ZeroHom α α).toFun (a * b) = (↑T : ZeroHom α α).toFun a * b
⊢ Membership.mem (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α)) T

Tactic:
refine ⟨⟨T, fun a b ↦ ?_, fun a b ↦ ?_⟩, rfl⟩
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g
a b : α
⊢ (↑T : ZeroHom α α).toFun (a * b) = a * (↑T : ZeroHom α α).toFun b

Tactic:
congr($(h (L a) (.inl ⟨a, rfl⟩)) b).symm

Premises used: AddMonoid.End.mulLeft, AddMonoid.End.instFunLike._aux_1, congrArg, id, Exists.intro, Or.inl, Eq.symm, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g
a b : α
⊢ (↑T : ZeroHom α α).toFun (a * b) = a * (↑T : ZeroHom α α).toFun b

Tactic:
exact congr($(h (L a) (.inl ⟨a, rfl⟩)) b).symm

Premises used: AddMonoid.End.mulLeft, congrArg, id, Exists.intro, Or.inl, Eq.symm, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g
a b : α
⊢ (↑T : ZeroHom α α).toFun (a * b) = (↑T : ZeroHom α α).toFun a * b

Tactic:
congr($(h (R b) (.inr ⟨b, rfl⟩)) a).symm

Premises used: AddMonoid.End.instFunLike._aux_1, congrArg, AddMonoid.End.mulRight, id, Exists.intro, Eq.symm, DFunLike.coe, Or.inr, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
T : AddMonoid.End α
h :
  ∀ (g : AddMonoid.End α),
    Membership.mem (γ := Set (AddMonoid.End α))
        (Set.range (ι := α) (⇑L : (a : α) → AddMonoid.End α) ∪ Set.range (ι := α) (⇑R : (a : α) → AddMonoid.End α)) g →
      g * T = T * g
a b : α
⊢ (↑T : ZeroHom α α).toFun (a * b) = (↑T : ZeroHom α α).toFun a * b

Tactic:
exact congr($(h (R b) (.inr ⟨b, rfl⟩)) a).symm

Premises used: congrArg, AddMonoid.End.mulRight, id, Exists.intro, Eq.symm, DFunLike.coe, Or.inr, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
rw :
  ∀ (g : CentroidHom α),
    g *
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
          CentroidHom α } =
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ } * g
⊢ Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α))
    { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }

Tactic:
rw [Subsemiring.mem_center_iff]

Premises used: Subsemiring.mem_center_iff
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
g : CentroidHom α
h :
  ∀ (a : α),
    Eq (α := α)
      ((g *
              { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
                CentroidHom α } :
            (a : α) → α)
          a :
        α)
      (({ toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
                CentroidHom α } *
              g :
            (a : α) → α)
          a :
        α)
⊢ g *
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
        CentroidHom α } =
    { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ } * g

Tactic:
ext a
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
g : CentroidHom α
a : α
⊢ Eq (α := α)
    ((g *
            { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
              CentroidHom α } :
          (a : α) → α)
        a :
      α)
    (({ toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
              CentroidHom α } *
            g :
          (a : α) → α)
        a :
      α)

Tactic:
map_mul_left g (↑z) a

Premises used: CentroidHomClass.map_mul_left
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
g : CentroidHom α
a : α
⊢ Eq (α := α)
    ((g *
            { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
              CentroidHom α } :
          (a : α) → α)
        a :
      α)
    (({ toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
              CentroidHom α } *
            g :
          (a : α) → α)
        a :
      α)

Tactic:
exact map_mul_left g (↑z) a

Premises used: CentroidHomClass.map_mul_left
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
z₁ z₂ : ↥(NonUnitalSubsemiring.center α)
a : α
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : CentroidHom α) ↦
                Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
                { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑(z₁ * z₂) : α), map_mul_left' := ⋯,
                  map_mul_right' := ⋯ : CentroidHom α }
                ⋯) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
    (((↑(HMul.hMul (α := ↥(Subsemiring.center (CentroidHom α)))
                (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑z₁ : α);
                Subtype.mk (p := fun (x : CentroidHom α) ↦
                  Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
                  { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z₁ : α), map_mul_left' := ⋯,
                    map_mul_right' := ⋯ : CentroidHom α }
                  ⋯)
                (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑z₂ : α);
                Subtype.mk (p := fun (x : CentroidHom α) ↦
                  Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
                  { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z₂ : α), map_mul_left' := ⋯,
                    map_mul_right' := ⋯ : CentroidHom α }
                  ⋯)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)

Tactic:
(z₁.prop.left_assoc z₂ a).symm

Premises used: Subtype.prop, IsMulCentral.left_assoc, Eq.symm, Subtype.val
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
z₁ z₂ : ↥(NonUnitalSubsemiring.center α)
a : α
⊢ Eq (α := α)
    (((↑(Subtype.mk (p := fun (x : CentroidHom α) ↦
                Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
                { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑(z₁ * z₂) : α), map_mul_left' := ⋯,
                  map_mul_right' := ⋯ : CentroidHom α }
                ⋯) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
    (((↑(HMul.hMul (α := ↥(Subsemiring.center (CentroidHom α)))
                (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑z₁ : α);
                Subtype.mk (p := fun (x : CentroidHom α) ↦
                  Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
                  { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z₁ : α), map_mul_left' := ⋯,
                    map_mul_right' := ⋯ : CentroidHom α }
                  ⋯)
                (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑z₂ : α);
                Subtype.mk (p := fun (x : CentroidHom α) ↦
                  Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
                  { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑z₂ : α), map_mul_left' := ⋯,
                    map_mul_right' := ⋯ : CentroidHom α }
                  ⋯)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)

Tactic:
exact (z₁.prop.left_assoc z₂ a).symm

Premises used: Subtype.prop, IsMulCentral.left_assoc, Eq.symm, Subtype.val
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
simp :
  Eq.{u_5 + 1} (α := ↥(Subsemiring.center (CentroidHom α)))
    (Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := 0, map_mul_left' := ⋯, map_mul_right' := ⋯ } ⋯)
    0
⊢ Eq.{u_5 + 1} (α := ↥(Subsemiring.center (CentroidHom α)))
    (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑0 : α);
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑0 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ } ⋯)
    0

Tactic:
simp only [ZeroMemClass.coe_zero, map_zero]

Premises used: map_zero, ZeroMemClass.coe_zero
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
⊢ Eq.{u_5 + 1} (α := ↥(Subsemiring.center (CentroidHom α)))
    (Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := 0, map_mul_left' := ⋯, map_mul_right' := ⋯ } ⋯)
    0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R_1 : Type u_4
α : Type u_5
inst : NonUnitalNonAssocSemiring α
inst_1 : Monoid M
inst_2 : Monoid N
inst_3 : Semiring R_1
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_1 α
inst_11 : SMulCommClass R_1 α α
inst_12 : IsScalarTower R_1 α α
R : Type u_6
inst_13 : CommSemiring «R»
inst_14 : Module «R» α
inst_15 : SMulCommClass «R» α α
inst_16 : IsScalarTower «R» α α
⊢ Eq.{u_5 + 1} (α := ↥(Subsemiring.center (CentroidHom α)))
    (Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := 0, map_mul_left' := ⋯, map_mul_right' := ⋯ } ⋯)
    0

Tactic:
exact rfl

Premises used: rfl