-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
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 α)
⊢ (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 α }
        ⋯)
have 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' := sorry,
                  map_mul_right' := sorry : CentroidHom α }
                sorry) :
            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' := sorry,
                    map_mul_right' := sorry : CentroidHom α }
                  sorry)
                (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' := sorry,
                    map_mul_right' := sorry : CentroidHom α }
                  sorry)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
Tactic: ext a