-- Module: Mathlib.Algebra.Polynomial.Module.Basic
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)
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)
single₃ :
  HAdd.hAdd (β := 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))
      ((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)
single₄ :
  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) +
      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) =
    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)
single₅ single₆ :
  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) +
      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) =
    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) +
      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)
⊢ (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)

Tactic:
rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]

Premises used: map_add, add_smul, Polynomial.eval_add