-- Lean 4 proof step from Mathlib.Algebra.Algebra.Unitization (goal)
Goal:
S : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring R
inst_2 : NonUnitalSemiring A
inst_3 : Module R A
inst_4 : IsScalarTower R A A
inst_5 : SMulCommClass R A A
inst_6 : Algebra S R
inst_7 : DistribMulAction S A
inst_8 : IsScalarTower S R A
s : S
r : R
a : A
inl_add_inr :
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
inl_add_inr₁ :
  HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        (inl r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl r)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
inl_add_inr₂ :
  inl (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) s : R) r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl r)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
inl_add_inr₃ :
  inl (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) s : R) r) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
        ((↑a : Unitization R A) : Unitization R A) =
    inl (HMul.hMul (β := R) r ((algebraMap S R : (a : S) → R) s : R)) +
      HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
        (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
⊢ HMul.hMul (α := Unitization R A) (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
      (inl r + (↑a : Unitization R A)) =
    HMul.hMul (β := Unitization R A) (inl r + (↑a : Unitization R A))
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
have inl_add_inr₄ : inl (HMul.hMul (α := R) ((algebraMap S R : (a : S) → R) s : R) r) +
    (↑(HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((algebraMap S R : (a : S) → R) s : R) a) : Unitization R A) =
  inl (HMul.hMul (β := R) r ((algebraMap S R : (a : S) → R) s : R)) +
    HMul.hMul (α := Unitization R A) (β := Unitization R A) ((↑a : Unitization R A) : Unitization R A)
      (inl ((algebraMap S R : (a : S) → R) s) : Unitization R A)
Tactic: rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]