-- Lean 4 proof step from Mathlib.Algebra.Ring.CentroidHom (goal)
Goal:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a r : α
h₁ :
  HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) *
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₂ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) -
      HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
        (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    0
h₃ :
  HMul.hMul (α := α) ((f * g : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α)) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
h₄ :
  (f * g : (a : α) → α)
      (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) =
    HMul.hMul (α := α) ((g * f : (a : α) → α) a : α)
      (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))
h₅ :
  Eq (α := α)
    ((f * g : (a : α) → α)
        (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) :
      α)
    ((g * f : (a : α) → α)
        (a * (r * HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α))) :
      α)
h₆ :
  Eq (α := α)
    (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α)
        (a *
          (r *
            HSub.hSub (α := α) (β := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a : α)
              ((g * f : (a : α) → α) a : α))) :
      α)
    ((g * f : (a : α) → α)
        (a *
          (r *
            HSub.hSub (α := α) (β := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a : α)
              ((g * f : (a : α) → α) a : α))) :
      α)
h₇ :
  Eq (α := α)
    (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α)
      (a *
        (r *
          HSub.hSub (α := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a)
            (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α) a))))
    (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α)
      (a *
        (r *
          HSub.hSub (α := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a)
            (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α) a))))
⊢ HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) * r *
      HSub.hSub (α := α) (β := α) ((f * g : (a : α) → α) a : α) ((g * f : (a : α) → α) a : α) =
    0
have h₈ : Eq (α := α)
  (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α)
    (a *
      (r *
        HSub.hSub (α := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a)
          (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α) a))))
  (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α)
    (a *
      (r *
        HSub.hSub (α := α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α) a)
          (Function.comp (β := α) (⇑g : (a : α) → α) (⇑f : (a : α) → α) a))))
Tactic: rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul,
        comp_mul_comm]