-- Lean 4 proof step from Mathlib.Algebra.TrivSqZeroExt.Basic (goal)
Goal:
S : Type u_1
R R' : Type u
M : Type v
inst : CommSemiring S
inst_1 : Semiring R
inst_2 : CommSemiring R'
inst_3 : AddCommMonoid M
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : Module R M
inst_7 : Module.{u, v} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower S R M
inst_10 : IsScalarTower.{u_1, u, v} S Rᵐᵒᵖ M
inst_11 : Module R' M
inst_12 : Module.{u, v} R'ᵐᵒᵖ M
inst_13 : IsCentralScalar R' M
A : Type u_2
inst_14 : Semiring A
inst_15 : Algebra S A
inst_16 : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((g : (a : M) → A) y : A) = 0
hfg :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (r •> x) = HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r : A) ((g : (a : M) → A) x : A)
hgf :
  ∀ (r : R) (x : M),
    (g : (a : M) → A) (x <• r) = HMul.hMul (α := A) (β := A) ((g : (a : M) → A) x : A) ((f : (a : R) → A) r : A)
r₁ : R
m₁ : M
r₂ : R
m₂ : M
rw :
  HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
rw₁ :
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (r₁ •> m₂) : A) ((g : (a : M) → A) (m₁ <• r₂) : A)) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
rw₂ :
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (m₁ <• r₂) : A) ((g : (a : M) → A) (r₁ •> m₂) : A)) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
        (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A)) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
rw₃ :
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HAdd.hAdd (α := A) (β := A) ((g : (a : M) → A) (m₁ <• r₂) : A) ((g : (a : M) → A) (r₁ •> m₂) : A)) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A))
rw₄ :
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HAdd.hAdd (α := A) ((g : (a : M) → A) (m₁ <• r₂) : A)
        (HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A))) =
    HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
      (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
        HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A))
⊢ HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ * r₂) : A) ((g : (a : M) → A) (r₁ •> m₂ + m₁ <• r₂) : A) =
    HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((f : (a : R) → A) r₂ : A) +
        HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)
have rw₅ : HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
    (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A)) =
  HAdd.hAdd (α := A) ((f : (a : R) → A) (r₁ * r₂) : A)
    (HMul.hMul (α := A) (β := A) ((g : (a : M) → A) m₁ : A) ((f : (a : R) → A) r₂ : A) +
      HMul.hMul (α := A) (β := A) ((f : (a : R) → A) r₁ : A) ((g : (a : M) → A) m₂ : A))
Tactic: rw [← map_mul, map_add, add_comm (g _), add_assoc, hfg, hgf]