[GOAL]
R : Type u_1
M✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
⊢ IsScalarTower S R[X] (PolynomialModule R M)
[PROOFSTEP]
haveI : IsScalarTower R R[X] (PolynomialModule R M) := modulePolynomialOfEndo.isScalarTower _
[GOAL]
R : Type u_1
M✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
⊢ IsScalarTower S R[X] (PolynomialModule R M)
[PROOFSTEP]
constructor
[GOAL]
case smul_assoc
R : Type u_1
M✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
⊢ ∀ (x : S) (y : R[X]) (z : PolynomialModule R M), (x • y) • z = x • y • z
[PROOFSTEP]
intro x y z
[GOAL]
case smul_assoc
R : Type u_1
M✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
x : S
y : R[X]
z : PolynomialModule R M
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
j : ℕ
m : M
⊢ ↑(monomial i) r • ↑(single R j) m = ↑(single R (i + j)) (r • m)
[PROOFSTEP]
simp only [LinearMap.mul_apply, Polynomial.aeval_monomial, LinearMap.pow_apply, Module.algebraMap_end_apply,
  modulePolynomialOfEndo_smul_def]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[i] (↑(single R j) m) = ↑(single R (i + j)) (r • m)
[PROOFSTEP]
induction i generalizing r j m with
| zero =>
  rw [Nat.zero_eq, Function.iterate_zero, zero_add]
  exact Finsupp.smul_single r j m
| succ n hn =>
  rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
  congr 2
  rw [← Nat.succ_eq_one_add]
  exact Finsupp.mapDomain_single
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[i] (↑(single R j) m) = ↑(single R (i + j)) (r • m)
[PROOFSTEP]
induction i generalizing r j m with
| zero =>
  rw [Nat.zero_eq, Function.iterate_zero, zero_add]
  exact Finsupp.smul_single r j m
| succ n hn =>
  rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
  congr 2
  rw [← Nat.succ_eq_one_add]
  exact Finsupp.mapDomain_single
[GOAL]
case zero
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[Nat.zero] (↑(single R j) m) = ↑(single R (Nat.zero + j)) (r • m)
[PROOFSTEP]

| zero =>
  rw [Nat.zero_eq, Function.iterate_zero, zero_add]
  exact Finsupp.smul_single r j m
[GOAL]
case zero
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[Nat.zero] (↑(single R j) m) = ↑(single R (Nat.zero + j)) (r • m)
[PROOFSTEP]
rw [Nat.zero_eq, Function.iterate_zero, zero_add]
[GOAL]
case zero
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • id (↑(single R j) m) = ↑(single R j) (r • m)
[PROOFSTEP]
exact Finsupp.smul_single r j m
[GOAL]
case succ
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[Nat.succ n] (↑(single R j) m) = ↑(single R (Nat.succ n + j)) (r • m)
[PROOFSTEP]

| succ n hn =>
  rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
  congr 2
  rw [← Nat.succ_eq_one_add]
  exact Finsupp.mapDomain_single
[GOAL]
case succ
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[Nat.succ n] (↑(single R j) m) = ↑(single R (Nat.succ n + j)) (r • m)
[PROOFSTEP]
rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
[GOAL]
case succ
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(Finsupp.lmapDomain M R Nat.succ) (↑(single R j) m)) =
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R (1 + j)) m)
[PROOFSTEP]
congr 2
[GOAL]
case succ.e_a.e_a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ ↑(Finsupp.lmapDomain M R Nat.succ) (↑(single R j) m) = ↑(single R (1 + j)) m
[PROOFSTEP]
rw [← Nat.succ_eq_one_add]
[GOAL]
case succ.e_a.e_a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ ↑(Finsupp.lmapDomain M R Nat.succ) (↑(single R j) m) = ↑(single R (Nat.succ j)) m
[PROOFSTEP]
exact Finsupp.mapDomain_single
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
g : PolynomialModule R M
n : ℕ
⊢ ↑(↑(monomial i) r • g) n = if i ≤ n then r • ↑g (n - i) else 0
[PROOFSTEP]
induction' g using PolynomialModule.induction_linear with p q hp hq
[GOAL]
case h0
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
⊢ ↑(↑(monomial i) r • 0) n = if i ≤ n then r • ↑0 (n - i) else 0
[PROOFSTEP]
simp only [smul_zero, zero_apply, ite_self]
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ↑(↑(monomial i) r • p) n = if i ≤ n then r • ↑p (n - i) else 0
hq : ↑(↑(monomial i) r • q) n = if i ≤ n then r • ↑q (n - i) else 0
⊢ ↑(↑(monomial i) r • (p + q)) n = if i ≤ n then r • ↑(p + q) (n - i) else 0
[PROOFSTEP]
simp only [smul_add, add_apply, hp, hq]
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ↑(↑(monomial i) r • p) n = if i ≤ n then r • ↑p (n - i) else 0
hq : ↑(↑(monomial i) r • q) n = if i ≤ n then r • ↑q (n - i) else 0
⊢ ((if i ≤ n then r • ↑p (n - i) else 0) + if i ≤ n then r • ↑q (n - i) else 0) =
    if i ≤ n then r • ↑p (n - i) + r • ↑q (n - i) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ↑(↑(monomial i) r • p) n = if i ≤ n then r • ↑p (n - i) else 0
hq : ↑(↑(monomial i) r • q) n = if i ≤ n then r • ↑q (n - i) else 0
h✝ : i ≤ n
⊢ r • ↑p (n - i) + r • ↑q (n - i) = r • ↑p (n - i) + r • ↑q (n - i)
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ↑(↑(monomial i) r • p) n = if i ≤ n then r • ↑p (n - i) else 0
hq : ↑(↑(monomial i) r • q) n = if i ≤ n then r • ↑q (n - i) else 0
h✝ : ¬i ≤ n
⊢ 0 + 0 = 0
[PROOFSTEP]
exacts [rfl, zero_add 0]
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ ↑(↑(monomial i) r • ↑(single R a✝) b✝) n = if i ≤ n then r • ↑(↑(single R a✝) b✝) (n - i) else 0
[PROOFSTEP]
rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and]
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ (if i + a✝ = n then r • b✝ else 0) = if i ≤ n ∧ a✝ = n - i then r • b✝ else 0
[PROOFSTEP]
congr
[GOAL]
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ (i + a✝ = n) = (i ≤ n ∧ a✝ = n - i)
[PROOFSTEP]
rw [eq_iff_iff]
[GOAL]
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n ↔ i ≤ n ∧ a✝ = n - i
[PROOFSTEP]
constructor
[GOAL]
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n → i ≤ n ∧ a✝ = n - i
[PROOFSTEP]
rintro rfl
[GOAL]
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
a✝ : ℕ
b✝ : M
⊢ i ≤ i + a✝ ∧ a✝ = i + a✝ - i
[PROOFSTEP]
simp
[GOAL]
case hsingle.e_c.mpr
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i ≤ n ∧ a✝ = n - i → i + a✝ = n
[PROOFSTEP]
rintro ⟨e, rfl⟩
[GOAL]
case hsingle.e_c.mpr.intro
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
b✝ : M
e : i ≤ n
⊢ i + (n - i) = n
[PROOFSTEP]
rw [add_comm, tsub_add_cancel_of_le e]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
f : R[X]
m : M
n : ℕ
⊢ ↑(f • ↑(single R i) m) n = if i ≤ n then coeff f (n - i) • m else 0
[PROOFSTEP]
induction' f using Polynomial.induction_on' with p q hp hq
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : ↑(p • ↑(single R i) m) n = if i ≤ n then coeff p (n - i) • m else 0
hq : ↑(q • ↑(single R i) m) n = if i ≤ n then coeff q (n - i) • m else 0
⊢ ↑((p + q) • ↑(single R i) m) n = if i ≤ n then coeff (p + q) (n - i) • m else 0
[PROOFSTEP]
rw [add_smul, Finsupp.add_apply, hp, hq, coeff_add, add_smul]
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : ↑(p • ↑(single R i) m) n = if i ≤ n then coeff p (n - i) • m else 0
hq : ↑(q • ↑(single R i) m) n = if i ≤ n then coeff q (n - i) • m else 0
⊢ ((if i ≤ n then coeff p (n - i) • m else 0) + if i ≤ n then coeff q (n - i) • m else 0) =
    if i ≤ n then coeff p (n - i) • m + coeff q (n - i) • m else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : ↑(p • ↑(single R i) m) n = if i ≤ n then coeff p (n - i) • m else 0
hq : ↑(q • ↑(single R i) m) n = if i ≤ n then coeff q (n - i) • m else 0
h✝ : i ≤ n
⊢ coeff p (n - i) • m + coeff q (n - i) • m = coeff p (n - i) • m + coeff q (n - i) • m
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : ↑(p • ↑(single R i) m) n = if i ≤ n then coeff p (n - i) • m else 0
hq : ↑(q • ↑(single R i) m) n = if i ≤ n then coeff q (n - i) • m else 0
h✝ : ¬i ≤ n
⊢ 0 + 0 = 0
[PROOFSTEP]
exacts [rfl, zero_add 0]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ ↑(↑(monomial n✝) a✝ • ↑(single R i) m) n = if i ≤ n then coeff (↑(monomial n✝) a✝) (n - i) • m else 0
[PROOFSTEP]
rw [monomial_smul_single, single_apply, coeff_monomial, ite_smul, zero_smul]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0
[PROOFSTEP]
by_cases h : i ≤ n
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : i ≤ n
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0
[PROOFSTEP]
simp_rw [eq_tsub_iff_add_eq_of_le h, if_pos h]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0
[PROOFSTEP]
rw [if_neg h, ite_eq_right_iff]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
⊢ n✝ + i = n → a✝ • m = 0
[PROOFSTEP]
intro e
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
e : n✝ + i = n
⊢ a✝ • m = 0
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
e : n✝ + i = n
⊢ False
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
f : R[X]
g : PolynomialModule R M
n : ℕ
⊢ ↑(f • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff f x.fst • ↑g x.snd
[PROOFSTEP]
induction' f using Polynomial.induction_on' with p q hp hq f_n f_a
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : ↑(p • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff p x.fst • ↑g x.snd
hq : ↑(q • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff q x.fst • ↑g x.snd
⊢ ↑((p + q) • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff (p + q) x.fst • ↑g x.snd
[PROOFSTEP]
rw [add_smul, Finsupp.add_apply, hp, hq, ← Finset.sum_add_distrib]
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : ↑(p • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff p x.fst • ↑g x.snd
hq : ↑(q • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff q x.fst • ↑g x.snd
⊢ ∑ x in Finset.Nat.antidiagonal n, (coeff p x.fst • ↑g x.snd + coeff q x.fst • ↑g x.snd) =
    ∑ x in Finset.Nat.antidiagonal n, coeff (p + q) x.fst • ↑g x.snd
[PROOFSTEP]
congr
[GOAL]
case h_add.e_f
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : ↑(p • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff p x.fst • ↑g x.snd
hq : ↑(q • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff q x.fst • ↑g x.snd
⊢ (fun x => coeff p x.fst • ↑g x.snd + coeff q x.fst • ↑g x.snd) = fun x => coeff (p + q) x.fst • ↑g x.snd
[PROOFSTEP]
ext
[GOAL]
case h_add.e_f.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : ↑(p • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff p x.fst • ↑g x.snd
hq : ↑(q • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff q x.fst • ↑g x.snd
x✝ : ℕ × ℕ
⊢ coeff p x✝.fst • ↑g x✝.snd + coeff q x✝.fst • ↑g x✝.snd = coeff (p + q) x✝.fst • ↑g x✝.snd
[PROOFSTEP]
rw [coeff_add, add_smul]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ ↑(↑(monomial f_n) f_a • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff (↑(monomial f_n) f_a) x.fst • ↑g x.snd
[PROOFSTEP]
rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => (monomial f_n f_a).coeff i • g j, monomial_smul_apply]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ≤ n then f_a • ↑g (n - f_n) else 0) =
    ∑ k in Finset.range (Nat.succ n), coeff (↑(monomial f_n) f_a) k • ↑g (n - k)
[PROOFSTEP]
simp_rw [Polynomial.coeff_monomial, ← Finset.mem_range_succ_iff]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ∈ Finset.range (Nat.succ n) then f_a • ↑g (n - f_n) else 0) =
    ∑ x in Finset.range (Nat.succ n), (if f_n = x then f_a else 0) • ↑g (n - x)
[PROOFSTEP]
rw [← Finset.sum_ite_eq (Finset.range (Nat.succ n)) f_n (fun x => f_a • g (n - x))]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (∑ x in Finset.range (Nat.succ n), if f_n = x then f_a • ↑g (n - x) else 0) =
    ∑ x in Finset.range (Nat.succ n), (if f_n = x then f_a else 0) • ↑g (n - x)
[PROOFSTEP]
congr
[GOAL]
case h_monomial.e_f
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (fun x => if f_n = x then f_a • ↑g (n - x) else 0) = fun x => (if f_n = x then f_a else 0) • ↑g (n - x)
[PROOFSTEP]
ext x
[GOAL]
case h_monomial.e_f.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
⊢ (if f_n = x then f_a • ↑g (n - x) else 0) = (if f_n = x then f_a else 0) • ↑g (n - x)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
h✝ : f_n = x
⊢ f_a • ↑g (n - x) = f_a • ↑g (n - x)
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
h✝ : ¬f_n = x
⊢ 0 = 0 • ↑g (n - x)
[PROOFSTEP]
exacts [rfl, (zero_smul R _).symm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
x : PolynomialModule R R
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : AddMonoidAlgebra R ℕ),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • x) =
    ↑(RingHom.id R[X]) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : AddMonoidAlgebra R ℕ),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        x
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
x : PolynomialModule R R
⊢ ↑(↑(toFinsuppIso R)).symm (r • x) = r * ↑(↑(toFinsuppIso R)).symm x
[PROOFSTEP]
rw [← RingEquiv.coe_toEquiv_symm, RingEquiv.coe_toEquiv]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
x : PolynomialModule R R
⊢ ↑(RingEquiv.symm (toFinsuppIso R)) (r • x) = r * ↑(RingEquiv.symm (toFinsuppIso R)) x
[PROOFSTEP]
induction' x using induction_linear with _ _ hp hq n a
[GOAL]
case h0
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
⊢ ↑(RingEquiv.symm (toFinsuppIso R)) (r • 0) = r * ↑(RingEquiv.symm (toFinsuppIso R)) 0
[PROOFSTEP]
rw [smul_zero, map_zero, mul_zero]
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
f✝ g✝ : PolynomialModule R R
hp : ↑(RingEquiv.symm (toFinsuppIso R)) (r • f✝) = r * ↑(RingEquiv.symm (toFinsuppIso R)) f✝
hq : ↑(RingEquiv.symm (toFinsuppIso R)) (r • g✝) = r * ↑(RingEquiv.symm (toFinsuppIso R)) g✝
⊢ ↑(RingEquiv.symm (toFinsuppIso R)) (r • (f✝ + g✝)) = r * ↑(RingEquiv.symm (toFinsuppIso R)) (f✝ + g✝)
[PROOFSTEP]
rw [smul_add, map_add, map_add, mul_add, hp, hq]
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
⊢ ↑(RingEquiv.symm (toFinsuppIso R)) (r • ↑(single R n) a) = r * ↑(RingEquiv.symm (toFinsuppIso R)) (↑(single R n) a)
[PROOFSTEP]
ext i
[GOAL]
case hsingle.a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
⊢ coeff (↑(RingEquiv.symm (toFinsuppIso R)) (r • ↑(single R n) a)) i =
    coeff (r * ↑(RingEquiv.symm (toFinsuppIso R)) (↑(single R n) a)) i
[PROOFSTEP]
simp only [coeff_ofFinsupp, smul_single_apply, toFinsuppIso_symm_apply, coeff_ofFinsupp, single_apply, ge_iff_le,
  smul_eq_mul, Polynomial.coeff_mul, mul_ite, mul_zero]
[GOAL]
case hsingle.a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
⊢ (if n ≤ i then coeff r (i - n) * a else 0) =
    ∑ x in Finset.Nat.antidiagonal i, if n = x.snd then coeff r x.fst * a else 0
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ coeff r (i - n) * a = ∑ x in Finset.Nat.antidiagonal i, if n = x.snd then coeff r x.fst * a else 0
[PROOFSTEP]
rw [Finset.sum_eq_single (i - n, n)]
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ coeff r (i - n) * a = if n = (i - n, n).snd then coeff r (i - n, n).fst * a else 0
case pos.h₀
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal i → b ≠ (i - n, n) → (if n = b.snd then coeff r b.fst * a else 0) = 0
case pos.h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ ¬(i - n, n) ∈ Finset.Nat.antidiagonal i → (if n = (i - n, n).snd then coeff r (i - n, n).fst * a else 0) = 0
[PROOFSTEP]
simp only [ite_true]
[GOAL]
case pos.h₀
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal i → b ≠ (i - n, n) → (if n = b.snd then coeff r b.fst * a else 0) = 0
[PROOFSTEP]
rintro ⟨p, q⟩ hpq1 hpq2
[GOAL]
case pos.h₀.mk
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q) ∈ Finset.Nat.antidiagonal i
hpq2 : (p, q) ≠ (i - n, n)
⊢ (if n = (p, q).snd then coeff r (p, q).fst * a else 0) = 0
[PROOFSTEP]
rw [Finset.Nat.mem_antidiagonal] at hpq1 
[GOAL]
case pos.h₀.mk
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
⊢ (if n = (p, q).snd then coeff r (p, q).fst * a else 0) = 0
[PROOFSTEP]
split_ifs with H
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = (p, q).snd
⊢ coeff r (p, q).fst * a = 0
[PROOFSTEP]
dsimp at H 
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ coeff r (p, q).fst * a = 0
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ False
[PROOFSTEP]
apply hpq2
[GOAL]
case pos.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ (p, q) = (i - n, n)
[PROOFSTEP]
rw [← hpq1, H]
[GOAL]
case pos.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ (p, q) = ((p, q).fst + (p, q).snd - q, q)
[PROOFSTEP]
simp only [add_le_iff_nonpos_left, nonpos_iff_eq_zero, add_tsub_cancel_right]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : ¬n = (p, q).snd
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case pos.h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ ¬(i - n, n) ∈ Finset.Nat.antidiagonal i → (if n = (i - n, n).snd then coeff r (i - n, n).fst * a else 0) = 0
[PROOFSTEP]
intro H
[GOAL]
case pos.h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : ¬(i - n, n) ∈ Finset.Nat.antidiagonal i
⊢ (if n = (i - n, n).snd then coeff r (i - n, n).fst * a else 0) = 0
[PROOFSTEP]
exfalso
[GOAL]
case pos.h₁.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : ¬(i - n, n) ∈ Finset.Nat.antidiagonal i
⊢ False
[PROOFSTEP]
apply H
[GOAL]
case pos.h₁.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : ¬(i - n, n) ∈ Finset.Nat.antidiagonal i
⊢ (i - n, n) ∈ Finset.Nat.antidiagonal i
[PROOFSTEP]
rw [Finset.Nat.mem_antidiagonal, tsub_add_cancel_of_le hn]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ 0 = ∑ x in Finset.Nat.antidiagonal i, if n = x.snd then coeff r x.fst * a else 0
[PROOFSTEP]
symm
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ (∑ x in Finset.Nat.antidiagonal i, if n = x.snd then coeff r x.fst * a else 0) = 0
[PROOFSTEP]
rw [Finset.sum_ite_of_false, Finset.sum_const_zero]
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ ∀ (x : ℕ × ℕ), x ∈ Finset.Nat.antidiagonal i → ¬n = x.snd
[PROOFSTEP]
simp_rw [Finset.Nat.mem_antidiagonal]
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ ∀ (x : ℕ × ℕ), x.fst + x.snd = i → ¬n = x.snd
[PROOFSTEP]
intro x hx
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
x : ℕ × ℕ
hx : x.fst + x.snd = i
⊢ ¬n = x.snd
[PROOFSTEP]
contrapose! hn
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
x : ℕ × ℕ
hx : x.fst + x.snd = i
hn : n = x.snd
⊢ n ≤ i
[PROOFSTEP]
rw [add_comm, ← hn] at hx 
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
x : ℕ × ℕ
hx : n + x.fst = i
hn : n = x.snd
⊢ n ≤ i
[PROOFSTEP]
exact Nat.le.intro hx
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ ↑(map R' f) (p • q) = Polynomial.map (algebraMap R R') p • ↑(map R' f) q
[PROOFSTEP]
apply induction_linear q
[GOAL]
case h0
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ ↑(map R' f) (p • 0) = Polynomial.map (algebraMap R R') p • ↑(map R' f) 0
[PROOFSTEP]
rw [smul_zero, map_zero, smul_zero]
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ ∀ (f_1 g : PolynomialModule R M),
    ↑(map R' f) (p • f_1) = Polynomial.map (algebraMap R R') p • ↑(map R' f) f_1 →
      ↑(map R' f) (p • g) = Polynomial.map (algebraMap R R') p • ↑(map R' f) g →
        ↑(map R' f) (p • (f_1 + g)) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (f_1 + g)
[PROOFSTEP]
intro f g e₁ e₂
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
q f g : PolynomialModule R M
e₁ : ↑(map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) f
e₂ : ↑(map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) g
⊢ ↑(map R' f✝) (p • (f + g)) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) (f + g)
[PROOFSTEP]
rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ ∀ (a : ℕ) (b : M),
    ↑(map R' f) (p • ↑(single R a) b) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (↑(single R a) b)
[PROOFSTEP]
intro i m
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
i : ℕ
m : M
⊢ ↑(map R' f) (p • ↑(single R i) m) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (↑(single R i) m)
[PROOFSTEP]
induction' p using Polynomial.induction_on' with _ _ e₁ e₂
[GOAL]
case hsingle.h_add
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : ↑(map R' f) (p✝ • ↑(single R i) m) = Polynomial.map (algebraMap R R') p✝ • ↑(map R' f) (↑(single R i) m)
e₂ : ↑(map R' f) (q✝ • ↑(single R i) m) = Polynomial.map (algebraMap R R') q✝ • ↑(map R' f) (↑(single R i) m)
⊢ ↑(map R' f) ((p✝ + q✝) • ↑(single R i) m) = Polynomial.map (algebraMap R R') (p✝ + q✝) • ↑(map R' f) (↑(single R i) m)
[PROOFSTEP]
rw [add_smul, map_add, e₁, e₂, Polynomial.map_add, add_smul]
[GOAL]
case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ ↑(map R' f) (↑(monomial n✝) a✝ • ↑(single R i) m) =
    Polynomial.map (algebraMap R R') (↑(monomial n✝) a✝) • ↑(map R' f) (↑(single R i) m)
[PROOFSTEP]
rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single, monomial_smul_single, f.map_smul,
  algebraMap_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ AddHom.toFun
      { toFun := fun p => Finsupp.sum p fun i m => r ^ i • m,
        map_add' :=
          (_ :
            ∀ (x y : PolynomialModule R M),
              (Finsupp.sum (x + y) fun i m => r ^ i • m) =
                (Finsupp.sum x fun i m => r ^ i • m) + Finsupp.sum y fun i m => r ^ i • m) }
      (s • m) =
    ↑(RingHom.id R) s •
      AddHom.toFun
        { toFun := fun p => Finsupp.sum p fun i m => r ^ i • m,
          map_add' :=
            (_ :
              ∀ (x y : PolynomialModule R M),
                (Finsupp.sum (x + y) fun i m => r ^ i • m) =
                  (Finsupp.sum x fun i m => r ^ i • m) + Finsupp.sum y fun i m => r ^ i • m) }
        m
[PROOFSTEP]
refine' (Finsupp.sum_smul_index' _).trans _
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ ∀ (i : ℕ), r ^ i • 0 = 0
[PROOFSTEP]
exact fun i => smul_zero _
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (Finsupp.sum m fun i c => r ^ i • s • c) =
    ↑(RingHom.id R) s •
      AddHom.toFun
        { toFun := fun p => Finsupp.sum p fun i m => r ^ i • m,
          map_add' :=
            (_ :
              ∀ (x y : PolynomialModule R M),
                (Finsupp.sum (x + y) fun i m => r ^ i • m) =
                  (Finsupp.sum x fun i m => r ^ i • m) + Finsupp.sum y fun i m => r ^ i • m) }
        m
[PROOFSTEP]
simp_rw [RingHom.id_apply, Finsupp.smul_sum]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (Finsupp.sum m fun i c => r ^ i • s • c) = Finsupp.sum m fun a b => s • r ^ a • b
[PROOFSTEP]
congr
[GOAL]
case refine'_2.e_g
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (fun i c => r ^ i • s • c) = fun a b => s • r ^ a • b
[PROOFSTEP]
ext i c
[GOAL]
case refine'_2.e_g.h.h
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
i : ℕ
c : M
⊢ r ^ i • s • c = s • r ^ i • c
[PROOFSTEP]
rw [smul_comm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(eval r) (p • q) = Polynomial.eval r p • ↑(eval r) q
[PROOFSTEP]
apply induction_linear q
[GOAL]
case h0
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(eval r) (p • 0) = Polynomial.eval r p • ↑(eval r) 0
[PROOFSTEP]
rw [smul_zero, map_zero, smul_zero]
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R 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)
[PROOFSTEP]
intro f g e₁ e₂
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R 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)
[PROOFSTEP]
rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R 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)
[PROOFSTEP]
intro i m
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R 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)
[PROOFSTEP]
induction' p using Polynomial.induction_on' with _ _ e₁ e₂
[GOAL]
case hsingle.h_add
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R 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)
[PROOFSTEP]
rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
[GOAL]
case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R 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)
[PROOFSTEP]
rw [monomial_smul_single, eval_single, Polynomial.eval_monomial, eval_single, smul_comm, ← smul_smul, pow_add, mul_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) q) = ↑f (↑(eval r) q)
[PROOFSTEP]
apply induction_linear q
[GOAL]
case h0
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) 0) = ↑f (↑(eval r) 0)
[PROOFSTEP]
simp_rw [map_zero]
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ∀ (f_1 g : PolynomialModule R M),
    ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) f_1) = ↑f (↑(eval r) f_1) →
      ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) g) = ↑f (↑(eval r) g) →
        ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (f_1 + g)) = ↑f (↑(eval r) (f_1 + g))
[PROOFSTEP]
intro f g e₁ e₂
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
q : PolynomialModule R M
r : R
f g : PolynomialModule R M
e₁ : ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) f) = ↑f✝ (↑(eval r) f)
e₂ : ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) g) = ↑f✝ (↑(eval r) g)
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) (f + g)) = ↑f✝ (↑(eval r) (f + g))
[PROOFSTEP]
simp_rw [map_add, e₁, e₂]
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M), ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (↑(single R a) b)) = ↑f (↑(eval r) (↑(single R a) b))
[PROOFSTEP]
intro i m
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (↑(single R i) m)) = ↑f (↑(eval r) (↑(single R i) m))
[PROOFSTEP]
rw [map_single, eval_single, eval_single, f.map_smul, ← map_pow, algebraMap_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
i : ℕ
m : M
⊢ ↑(comp p) (↑(single R i) m) = p ^ i • ↑(single R 0) m
[PROOFSTEP]
rw [comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
i : ℕ
m : M
⊢ ↑(eval p) (↑(map R[X] (lsingle R 0)) (↑(single R i) m)) = p ^ i • ↑(single R 0) m
[PROOFSTEP]
erw [map_single, eval_single]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
i : ℕ
m : M
⊢ p ^ i • ↑(lsingle R 0) m = p ^ i • ↑(single R 0) m
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(eval r) (↑(comp p) q) = ↑(eval (Polynomial.eval r p)) q
[PROOFSTEP]
rw [← LinearMap.comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(LinearMap.comp (eval r) (comp p)) q = ↑(eval (Polynomial.eval r p)) q
[PROOFSTEP]
apply induction_linear q
[GOAL]
case h0
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(LinearMap.comp (eval r) (comp p)) 0 = ↑(eval (Polynomial.eval r p)) 0
[PROOFSTEP]
simp_rw [map_zero]
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (f g : PolynomialModule R M),
    ↑(LinearMap.comp (eval r) (comp p)) f = ↑(eval (Polynomial.eval r p)) f →
      ↑(LinearMap.comp (eval r) (comp p)) g = ↑(eval (Polynomial.eval r p)) g →
        ↑(LinearMap.comp (eval r) (comp p)) (f + g) = ↑(eval (Polynomial.eval r p)) (f + g)
[PROOFSTEP]
intro _ _ e₁ e₂
[GOAL]
case hadd
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
f✝ g✝ : PolynomialModule R M
e₁ : ↑(LinearMap.comp (eval r) (comp p)) f✝ = ↑(eval (Polynomial.eval r p)) f✝
e₂ : ↑(LinearMap.comp (eval r) (comp p)) g✝ = ↑(eval (Polynomial.eval r p)) g✝
⊢ ↑(LinearMap.comp (eval r) (comp p)) (f✝ + g✝) = ↑(eval (Polynomial.eval r p)) (f✝ + g✝)
[PROOFSTEP]
simp_rw [map_add, e₁, e₂]
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M),
    ↑(LinearMap.comp (eval r) (comp p)) (↑(single R a) b) = ↑(eval (Polynomial.eval r p)) (↑(single R a) b)
[PROOFSTEP]
intro i m
[GOAL]
case hsingle
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ ↑(LinearMap.comp (eval r) (comp p)) (↑(single R i) m) = ↑(eval (Polynomial.eval r p)) (↑(single R i) m)
[PROOFSTEP]
rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, pow_zero, one_smul, Polynomial.eval_pow]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p p' : R[X]
q : PolynomialModule R M
⊢ ↑(comp p) (p' • q) = Polynomial.comp p' p • ↑(comp p) q
[PROOFSTEP]
rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p p' : R[X]
q : PolynomialModule R M
⊢ eval₂ (algebraMap R R[X]) p p' • ↑(eval p) (↑(map R[X] (lsingle R 0)) q) =
    eval₂ C p p' • ↑(eval p) (↑(map R[X] (lsingle R 0)) q)
[PROOFSTEP]
rfl
