-- 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
⊢ (HAdd.hAdd (α := tsze R M →ₗ[S] A) (AlgHom.toLinearMap (f.comp (fstHom S R M)))
          (g ∘ₗ
            (↑S :
                {S_1 : Type u} →
                  {M : Type (max u v)} →
                    {M₂ : Type v} →
                      [inst : Semiring S] →
                        [inst_17 : Semiring S_1] →
                          [inst_18 : AddCommMonoid M] →
                            [inst_19 : AddCommMonoid M₂] →
                              [inst_20 : Module S M] →
                                [inst_21 : Module S M₂] →
                                  [inst_22 : Module S_1 M] →
                                    [inst_23 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (sndHom R M)) :
        (a : tsze R M) → A)
      ((inl r₁ + inr m₁) * (inl r₂ + inr m₂)) =
    HMul.hMul (α := A) (β := A)
      ((HAdd.hAdd (α := tsze R M →ₗ[S] A) (AlgHom.toLinearMap (f.comp (fstHom S R M)))
              (g ∘ₗ
                (↑S :
                    {S_1 : Type u} →
                      {M : Type (max u v)} →
                        {M₂ : Type v} →
                          [inst : Semiring S] →
                            [inst_17 : Semiring S_1] →
                              [inst_18 : AddCommMonoid M] →
                                [inst_19 : AddCommMonoid M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [inst_22 : Module S_1 M] →
                                        [inst_23 : Module S_1 M₂] →
                                          [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  (sndHom R M)) :
            (a : tsze R M) → A)
          (inl r₁ + inr m₁) :
        A)
      ((HAdd.hAdd (α := tsze R M →ₗ[S] A) (AlgHom.toLinearMap (f.comp (fstHom S R M)))
              (g ∘ₗ
                (↑S :
                    {S_1 : Type u} →
                      {M : Type (max u v)} →
                        {M₂ : Type v} →
                          [inst : Semiring S] →
                            [inst_17 : Semiring S_1] →
                              [inst_18 : AddCommMonoid M] →
                                [inst_19 : AddCommMonoid M₂] →
                                  [inst_20 : Module S M] →
                                    [inst_21 : Module S M₂] →
                                      [inst_22 : Module S_1 M] →
                                        [inst_23 : Module S_1 M₂] →
                                          [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  (sndHom R M)) :
            (a : tsze R M) → A)
          (inl r₂ + inr m₂) :
        A)
have dsimp : HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) ((r₁ + 0) * (r₂ + 0)) : A)
    ((g : (a : M) → A) ((r₁ + 0) •> (0 + m₂) + (op r₂ + 0) •> (0 + m₁)) : A) =
  HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₁ + 0) : A) ((g : (a : M) → A) (0 + m₁) : A) *
    HAdd.hAdd (α := A) (β := A) ((f : (a : R) → A) (r₂ + 0) : A) ((g : (a : M) → A) (0 + m₂) : A)
Tactic: dsimp