-- Mathlib/Algebra/Polynomial/Module/Basic.lean
@[simp]
lemma aeval_equivPolynomial {S : Type*} [CommRing S] [Algebra S R]
    (f : PolynomialModule S S) (x : R) :
    aeval x (equivPolynomial f) = eval x (map R (Algebra.linearMap S R) f)

Proof state:
case hadd
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
⊢ ∀ (f g : PolynomialModule S S),
    (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f) →
      (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g) →
        (aeval x) (equivPolynomial (f + g)) = (eval x) ((map R (Algebra.linearMap S R)) (f + g))

Tactic:
intro f g e₁ e₂

Result:
case hadd
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f✝ : PolynomialModule S S
x : R
f g : PolynomialModule S S
e₁ : (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)
e₂ : (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g)
⊢ (aeval x) (equivPolynomial (f + g)) = (eval x) ((map R (Algebra.linearMap S R)) (f + g))

Proof state:
case h0
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
⊢ (aeval x) (equivPolynomial 0) = (eval x) ((map R (Algebra.linearMap S R)) 0)

Tactic:
simp

Result:
no goals

Proof state:
case hsingle
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
⊢ ∀ (a : ℕ) (b : S),
    (aeval x) (equivPolynomial ((single S a) b)) = (eval x) ((map R (Algebra.linearMap S R)) ((single S a) b))

Tactic:
intro i m

Result:
case hsingle
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
i : ℕ
m : S
⊢ (aeval x) (equivPolynomial ((single S i) m)) = (eval x) ((map R (Algebra.linearMap S R)) ((single S i) m))

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
⊢ (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)

Tactic:
apply induction_linear f

Result:
case h0
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
⊢ (aeval x) (equivPolynomial 0) = (eval x) ((map R (Algebra.linearMap S R)) 0)

case hadd
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
⊢ ∀ (f g : PolynomialModule S S),
    (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f) →
      (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g) →
        (aeval x) (equivPolynomial (f + g)) = (eval x) ((map R (Algebra.linearMap S R)) (f + g))

case hsingle
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
⊢ ∀ (a : ℕ) (b : S),
    (aeval x) (equivPolynomial ((single S a) b)) = (eval x) ((map R (Algebra.linearMap S R)) ((single S a) b))

Proof state:
case hsingle
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f : PolynomialModule S S
x : R
i : ℕ
m : S
⊢ (aeval x) (equivPolynomial ((single S i) m)) = (eval x) ((map R (Algebra.linearMap S R)) ((single S i) m))

Tactic:
rw [equivPolynomial_single, aeval_monomial, mul_comm, map_single,
  Algebra.linearMap_apply, eval_single, smul_eq_mul]

Result:
no goals

Proof state:
case hadd
R : Type u_1
inst✝² : CommRing R
S : Type u_6
inst✝¹ : CommRing S
inst✝ : Algebra S R
f✝ : PolynomialModule S S
x : R
f g : PolynomialModule S S
e₁ : (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)
e₂ : (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g)
⊢ (aeval x) (equivPolynomial (f + g)) = (eval x) ((map R (Algebra.linearMap S R)) (f + g))

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

Result:
no goals