-- 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
r : R
i : ℕ
m : M
p q : R[X]
e₁ :
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) p
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r p)
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
e₂ :
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) q
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r q)
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
single :
  (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) p
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) +
        HSMul.hSMul (β := PolynomialModule R M) q
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
single₁ :
  HAdd.hAdd (α := M) (β := M)
      ((eval r : (a : PolynomialModule R M) → M)
          (HSMul.hSMul (β := PolynomialModule R M) p
            ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) :
        M)
      ((eval r : (a : PolynomialModule R M) → M)
          (HSMul.hSMul (β := PolynomialModule R M) q
            ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) :
        M) =
    HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
⊢ (eval r : (a : PolynomialModule R M) → M)
      (HSMul.hSMul (β := PolynomialModule R M) (p + q)
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (β := M) (Polynomial.eval r (p + q))
      ((eval r : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
have single₂ : HAdd.hAdd (α := M) (β := M)
    ((eval r : (a : PolynomialModule R M) → M)
        (HSMul.hSMul (β := PolynomialModule R M) p
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) :
      M)
    ((eval r : (a : PolynomialModule R M) → M)
        (HSMul.hSMul (β := PolynomialModule R M) q
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) :
      M) =
  HSMul.hSMul (β := M) (Polynomial.eval r p + Polynomial.eval r q)
    ((eval r : (a : PolynomialModule R M) → M)
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)
Tactic: rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]