-- 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 :
  ∀ (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 :
        α)
⊢ (let __src : AddMonoid.End α := (L : (a : α) → AddMonoid.End α) (↑(z₁ * z₂) : α);
    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' := ⋯ }
      ⋯) =
    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 α }
        ⋯)

Tactic:
ext a