-- Module: Mathlib.Algebra.Algebra.Unitization
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 :
  s • (inl r + (↑a : Unitization R A)) =
    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)
inl_add_inr₁ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    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)
inl_add_inr₂ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HMul.hMul (α := Unitization R A) (inl (HSMul.hSMul (β := R) s 1)) (inl r) +
      inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₃ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + inl (HSMul.hSMul (β := R) s 1) * (↑a : Unitization R A)
inl_add_inr₄ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (HSMul.hSMul (β := R) s 1 * r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
inl_add_inr₅ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    inl (s • r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
inl_add_inr₆ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HSMul.hSMul (β := Unitization R A) s (inl r) + (↑(HSMul.hSMul (β := R) s 1 • a) : Unitization R A)
inl_add_inr₇ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HSMul.hSMul (β := Unitization R A) s (inl r) +
      HSMul.hSMul (β := Unitization R A) (HSMul.hSMul (β := R) s 1) (↑a : Unitization R A)
inl_add_inr₈ inl_add_inr₉ :
  HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A) =
    HSMul.hSMul (β := Unitization R A) s (inl r) + HSMul.hSMul (β := Unitization R A) s (↑a : Unitization R A)
⊢ s • (inl r + (↑a : 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))

Tactic:
rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr,
        smul_one_mul, inl_smul, inr_smul, smul_one_smul]

Premises used: Unitization.inl_mul_inr, Unitization.inr_smul, Unitization.inl_mul_inl, Algebra.algebraMap_eq_smul_one, smul_one_smul, smul_one_mul, mul_add, Unitization.inl_smul, smul_add