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_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» α α
x x_1 : ↥(NonUnitalSubsemiring.center α)
dsimp :
  Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) ((↑x : α) + (↑x_1 : α)), map_mul_left' := ⋯,
        map_mul_right' := ⋯ : CentroidHom α }
      ⋯ =
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      (HAdd.hAdd (α := CentroidHom α)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ })
      ⋯
⊢ (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑(x + x_1) : α);
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑(x + x_1) : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }
      ⋯) =
    HAdd.hAdd (α := ↥(Subsemiring.center (CentroidHom α)))
      (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑x : α);
      Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
          CentroidHom α }
        ⋯)
      (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑x_1 : α);
      Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ :
          CentroidHom α }
        ⋯)

Tactic:
dsimp
-- 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» α α
x x_1 : ↥(NonUnitalSubsemiring.center α)
simp :
  Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      {
        toAddMonoidHom :=
          HAdd.hAdd (α := AddMonoid.End α) (β := AddMonoid.End α)
            ((L : (a : α) → AddMonoid.End α) (↑x : α) : AddMonoid.End α)
            ((L : (a : α) → AddMonoid.End α) (↑x_1 : α) : AddMonoid.End α),
        map_mul_left' := ⋯, map_mul_right' := ⋯ : CentroidHom α }
      ⋯ =
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      (HAdd.hAdd (α := CentroidHom α)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ })
      ⋯
⊢ Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) ((↑x : α) + (↑x_1 : α)), map_mul_left' := ⋯,
        map_mul_right' := ⋯ : CentroidHom α }
      ⋯ =
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      (HAdd.hAdd (α := CentroidHom α)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ })
      ⋯

Tactic:
simp only [map_add]

Premises used: map_add
-- 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» α α
x x_1 : ↥(NonUnitalSubsemiring.center α)
⊢ Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      {
        toAddMonoidHom :=
          HAdd.hAdd (α := AddMonoid.End α) (β := AddMonoid.End α)
            ((L : (a : α) → AddMonoid.End α) (↑x : α) : AddMonoid.End α)
            ((L : (a : α) → AddMonoid.End α) (↑x_1 : α) : AddMonoid.End α),
        map_mul_left' := ⋯, map_mul_right' := ⋯ : CentroidHom α }
      ⋯ =
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x)
      (HAdd.hAdd (α := CentroidHom α)
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x : α), map_mul_left' := ⋯, map_mul_right' := ⋯ }
        { toAddMonoidHom := (L : (a : α) → AddMonoid.End α) (↑x_1 : α), map_mul_left' := ⋯, map_mul_right' := ⋯ })
      ⋯

Tactic:
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» α α
f g : ↥(Subsemiring.center (CentroidHom α))
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun) f)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun) g)
mk :
  ∀ (val : CentroidHom α)
    (property : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val)
    (h :
      Eq.{u_5 + 1} (α := (a : α) → α)
        ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
          (Subtype.mk (p := fun (x : CentroidHom α) ↦
            Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
        ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
          g)),
    Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property =
      g
⊢ f = g

Tactic:
cases f
-- 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» α α
g : ↥(Subsemiring.center (CentroidHom α))
val : CentroidHom α
property : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun) g)
mk :
  ∀ (val_1 : CentroidHom α)
    (property_1 : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val_1)
    (h :
      Eq.{u_5 + 1} (α := (a : α) → α)
        ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
          (Subtype.mk (p := fun (x : CentroidHom α) ↦
            Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
        ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
          (Subtype.mk (p := fun (x : CentroidHom α) ↦
            Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1
            property_1))),
    Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property =
      Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1
⊢ Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property =
    g

Tactic:
cases g
-- 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» α α
val : CentroidHom α
property : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val
val_1 : CentroidHom α
property_1 : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val_1
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1))
mk : ∀ (x : α), Eq (α := α) ((val : (a : α) → α) x : α) ((val_1 : (a : α) → α) x : α)
⊢ Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property =
    Subtype.mk (p := fun (x : CentroidHom α) ↦
      Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1

Tactic:
congr with x
-- 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» α α
val : CentroidHom α
property : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val
val_1 : CentroidHom α
property_1 : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val_1
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1))
x : α
⊢ Eq (α := α) ((val : (a : α) → α) x : α) ((val_1 : (a : α) → α) x : α)

Tactic:
congrFun h x

Premises used: congrFun
-- 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» α α
val : CentroidHom α
property : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val
val_1 : CentroidHom α
property_1 : Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) val_1
h :
  Eq.{u_5 + 1} (α := (a : α) → α)
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val property))
    ((fun (f : ↥(Subsemiring.center (CentroidHom α))) ↦ (↑(↑f : CentroidHom α).toAddMonoidHom : ZeroHom α α).toFun)
      (Subtype.mk (p := fun (x : CentroidHom α) ↦
        Membership.mem (γ := Subsemiring (CentroidHom α)) (Subsemiring.center (CentroidHom α)) x) val_1 property_1))
x : α
⊢ Eq (α := α) ((val : (a : α) → α) x : α) ((val_1 : (a : α) → α) x : α)

Tactic:
exact congrFun h x

Premises used: congrFun
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
z : ↥(NonUnitalSubsemiring.center α)
a : α
⊢ (((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α))) z :
          ↥(Subsemiring.center (CentroidHom α))) :
        (a : α) → α)
      a =
    (↑z : α) * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
z : ↥(NonUnitalSubsemiring.center α)
a : α
⊢ (((centerToCentroid : (a : ↥(NonUnitalSubsemiring.center α)) → CentroidHom α) z : CentroidHom α) : (a : α) → α) a =
    (↑z : α) * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
mp :
  Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a →
    Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
mpr :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) →
    Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a ↔
    Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)

Tactic:
constructor
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a →
    Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)

Tactic:
fun ha ↦ ⟨AddMonoidHom.ext <| fun _ => (IsMulCentral.comm ha _).symm,
      ⟨centerToCentroid ⟨a, ha⟩, rfl⟩⟩

Premises used: CentroidHom.centerToCentroid, IsMulCentral.comm, AddMonoidHom.ext, Subtype.mk, Commute.symm, And.intro, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a →
    Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α) ∧
      Membership.mem (α := AddMonoid.End α) (γ := Subsemiring (AddMonoid.End α)) (RingHom.rangeS (toEndRingHom α))
        ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)

Tactic:
exact fun ha ↦ ⟨AddMonoidHom.ext <| fun _ => (IsMulCentral.comm ha _).symm,
      ⟨centerToCentroid ⟨a, ha⟩, rfl⟩⟩
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
⊢ ∀ (d : α), (T : (a : α) → α) d = a * d

Tactic:
have e1 (d : α) : T d = a * d := congr($hT d)
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
⊢ ∀ (d : α), (T : (a : α) → α) d = d * a

Tactic:
have e2 (d : α) : T d = d * a := congr($(hT.trans hc.symm) d)
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
constructor : ∀ (a_1 : α), Commute a a_1
constructor₁ : ∀ (b c : α), a * (b * c) = a * b * c
constructor₂ : ∀ (a_1 b : α), a_1 * b * a = a_1 * (b * a)
⊢ Membership.mem (γ := NonUnitalSubsemiring α) (NonUnitalSubsemiring.center α) a

Tactic:
constructor
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
⊢ ∀ (a_1 : α), Commute a a_1

Tactic:
(congr($hc.symm ·))

Premises used: congrArg, id, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
⊢ ∀ (a_1 : α), Commute a a_1

Tactic:
exact (congr($hc.symm ·))

Premises used: congrArg, id, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
⊢ ∀ (a_1 : α), Commute a a_1

Tactic:
case comm => exact (congr($hc.symm ·))

Premises used: comm, congrArg, id, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
⊢ ∀ (b c : α), a * (b * c) = a * b * c

Tactic:
simpa [e1] using (map_mul_right T · ·)

Premises used: CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Ring.CentroidHom
Goal:
α : Type u_5
inst : NonUnitalNonAssocSemiring α
a : α
hc :
  Eq (α := AddMonoid.End α) ((R : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
T : CentroidHom α
hT :
  Eq (α := AddMonoid.End α) ((toEndRingHom α : (a : CentroidHom α) → AddMonoid.End α) T : AddMonoid.End α)
    ((L : (a : α) → AddMonoid.End α) a : AddMonoid.End α)
e1 : ∀ (d : α), (T : (a : α) → α) d = a * d
e2 : ∀ (d : α), (T : (a : α) → α) d = d * a
⊢ ∀ (b c : α), a * (b * c) = a * b * c

Tactic:
case left_assoc => simpa [e1] using (map_mul_right T · ·)

Premises used: CentroidHomClass.map_mul_right