-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem comp_eval (p : R[X]) (q : PolynomialModule R M) (r : R) :
    eval r (comp p q) = eval (p.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 ∘ₗ comp p) f✝ = (eval (Polynomial.eval r p)) f✝
e₂ : (eval r ∘ₗ comp p) g✝ = (eval (Polynomial.eval r p)) g✝
⊢ (eval r ∘ₗ comp p) (f✝ + g✝) = (eval (Polynomial.eval r p)) (f✝ + g✝)

Tactic:
simp_rw [map_add, e₁, e₂]

Result:
no goals

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 ∘ₗ comp p) 0 = (eval (Polynomial.eval r p)) 0

Tactic:
simp_rw [map_zero]

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) ((comp p) q) = (eval (Polynomial.eval r p)) q

Tactic:
rw [← LinearMap.comp_apply]

Result:
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 ∘ₗ comp p) q = (eval (Polynomial.eval r p)) 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),
    (eval r ∘ₗ comp p) f = (eval (Polynomial.eval r p)) f →
      (eval r ∘ₗ comp p) g = (eval (Polynomial.eval r p)) g →
        (eval r ∘ₗ comp p) (f + g) = (eval (Polynomial.eval r p)) (f + g)

Tactic:
intro _ _ 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 ∘ₗ comp p) f✝ = (eval (Polynomial.eval r p)) f✝
e₂ : (eval r ∘ₗ comp p) g✝ = (eval (Polynomial.eval r p)) g✝
⊢ (eval r ∘ₗ comp p) (f✝ + g✝) = (eval (Polynomial.eval r p)) (f✝ + g✝)

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
⊢ Polynomial.eval r p ^ i • r ^ 0 • m = Polynomial.eval r p ^ 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
i : ℕ
m : M
⊢ (eval r ∘ₗ comp p) ((single R i) m) = (eval (Polynomial.eval r p)) ((single R i) m)

Tactic:
rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]

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
⊢ Polynomial.eval r p ^ i • r ^ 0 • m = Polynomial.eval r p ^ 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
⊢ ∀ (a : ℕ) (b : M), (eval r ∘ₗ comp p) ((single R a) b) = (eval (Polynomial.eval r p)) ((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 ∘ₗ comp p) ((single R i) m) = (eval (Polynomial.eval r p)) ((single R i) m)

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 ∘ₗ comp p) q = (eval (Polynomial.eval r p)) 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 ∘ₗ comp p) 0 = (eval (Polynomial.eval r p)) 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 ∘ₗ comp p) f = (eval (Polynomial.eval r p)) f →
      (eval r ∘ₗ comp p) g = (eval (Polynomial.eval r p)) g →
        (eval r ∘ₗ comp p) (f + g) = (eval (Polynomial.eval r p)) (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 ∘ₗ comp p) ((single R a) b) = (eval (Polynomial.eval r p)) ((single R a) b)