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.264988
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

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.264988
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
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.264988
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
induction' f using Polynomial.induction_on' with p q hp hq
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.264988
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
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.264988
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
rw [add_smul, Finsupp.add_apply, hp, hq, coeff_add, add_smul]
case h_add.inl
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.264988
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 h_add.inr
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.264988
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
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.264988
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
split_ifs
no goals
case h_add.inl
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.264988
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 h_add.inr
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.264988
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
exacts [rfl, zero_add 0]
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.264988
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
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.264988
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
rw [monomial_smul_single, single_apply, coeff_monomial, ite_smul, zero_smul]
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.264988
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

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.264988
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
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.264988
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
by_cases h : i ≤ n
no goals
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.264988
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
simp_rw [eq_tsub_iff_add_eq_of_le h, if_pos h]
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.264988
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
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.264988
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
rw [if_neg h, ite_eq_right_iff]
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.264988
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
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.264988
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
intro e
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.264988
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
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.264988
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
exfalso
no goals
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.264988
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
linarith