-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem eval_smul (p : R[X]) (q : PolynomialModule R M) (r : R) :
    eval r (p • q) = p.eval r • eval r q

Proof state:
case hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
f g : PolynomialModule R M
e₁ : (eval r) (p • f) = Polynomial.eval r p • (eval r) f
e₂ : (eval r) (p • g) = Polynomial.eval r p • (eval r) g
⊢ (eval r) (p • (f + g)) = Polynomial.eval r p • (eval r) (f + g)

Tactic:
rw [smul_add, map_add, e₁, e₂, map_add, smul_add]

Result:
no goals

Proof state:
case hsingle.h_add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
q : PolynomialModule R M
r : R
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (eval r) (p✝ • (single R i) m) = Polynomial.eval r p✝ • (eval r) ((single R i) m)
e₂ : (eval r) (q✝ • (single R i) m) = Polynomial.eval r q✝ • (eval r) ((single R i) m)
⊢ (eval r) ((p✝ + q✝) • (single R i) m) = Polynomial.eval r (p✝ + q✝) • (eval r) ((single R i) m)

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

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ (eval r) (p • q) = Polynomial.eval r p • (eval r) q

Tactic:
apply induction_linear q

Result:
case h0
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ (eval r) (p • 0) = Polynomial.eval r p • (eval r) 0

case hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (f g : PolynomialModule R M),
    (eval r) (p • f) = Polynomial.eval r p • (eval r) f →
      (eval r) (p • g) = Polynomial.eval r p • (eval r) g →
        (eval r) (p • (f + g)) = Polynomial.eval r p • (eval r) (f + g)

case hsingle
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M), (eval r) (p • (single R a) b) = Polynomial.eval r p • (eval r) ((single R a) b)

Proof state:
case h0
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ (eval r) (p • 0) = Polynomial.eval r p • (eval r) 0

Tactic:
rw [smul_zero, map_zero, smul_zero]

Result:
no goals

Proof state:
case hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (f g : PolynomialModule R M),
    (eval r) (p • f) = Polynomial.eval r p • (eval r) f →
      (eval r) (p • g) = Polynomial.eval r p • (eval r) g →
        (eval r) (p • (f + g)) = Polynomial.eval r p • (eval r) (f + g)

Tactic:
intro f g e₁ e₂

Result:
case hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
f g : PolynomialModule R M
e₁ : (eval r) (p • f) = Polynomial.eval r p • (eval r) f
e₂ : (eval r) (p • g) = Polynomial.eval r p • (eval r) g
⊢ (eval r) (p • (f + g)) = Polynomial.eval r p • (eval r) (f + g)

Proof state:
case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
q : PolynomialModule R M
r : R
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ (eval r) ((monomial n✝) a✝ • (single R i) m) = Polynomial.eval r ((monomial n✝) a✝) • (eval r) ((single R i) m)

Tactic:
simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]

Result:
case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
q : PolynomialModule R M
r : R
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ r ^ (n✝ + i) • a✝ • m = (a✝ * r ^ n✝) • r ^ i • m

Proof state:
case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
q : PolynomialModule R M
r : R
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ r ^ (n✝ + i) • a✝ • m = (a✝ * r ^ n✝) • r ^ i • m

Tactic:
module

Result:
no goals

Proof state:
case hsingle
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M), (eval r) (p • (single R a) b) = Polynomial.eval r p • (eval r) ((single R a) b)

Tactic:
intro i m

Result:
case hsingle
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ (eval r) (p • (single R i) m) = Polynomial.eval r p • (eval r) ((single R i) m)

Proof state:
case hsingle
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ (eval r) (p • (single R i) m) = Polynomial.eval r p • (eval r) ((single R i) m)

Tactic:
induction p using Polynomial.induction_on' with
| h_add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
| h_monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module

Result:
no goals