-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
f g : PolynomialModule R R
hp :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
hq :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
add :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f + r • g) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
add₁ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
add₂ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    r *
      HAdd.hAdd (α := R[X]) (β := R[X]) ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X])
        ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
add₃ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) : R[X])
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
add₄ :
  HAdd.hAdd (β := R[X])
      (HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]))
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) : R[X]) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • (f + g)) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
have add₅ : HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]) +
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X]) =
  HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]) +
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])
Tactic: rw [smul_add, map_add, map_add, mul_add, hp, hq]