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

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.304250
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
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.304250
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
induction' f using Polynomial.induction_on' with p q hp hq f_n f_a
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.304250
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
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.304250
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
rw [add_smul, Finsupp.add_apply, hp, hq, ← Finset.sum_add_distrib]
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.304250
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
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.304250
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
congr
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.304250
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
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.304250
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
ext
no goals
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.304250
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
rw [coeff_add, add_smul]
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.304250
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)
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.304250
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
rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => (monomial f_n f_a).coeff i • g j,
  monomial_smul_apply]
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.304250
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)
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.304250
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)
simp_rw [Polynomial.coeff_monomial, ← Finset.mem_range_succ_iff]
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.304250
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)
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.304250
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)
rw [← Finset.sum_ite_eq (Finset.range (Nat.succ n)) f_n (fun x => f_a • g (n - x))]
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.304250
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)
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.304250
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)
congr
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.304250
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)
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.304250
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)
ext x
case h_monomial.e_f.h.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.304250
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 h_monomial.e_f.h.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.304250
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)
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.304250
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)
split_ifs
no goals
case h_monomial.e_f.h.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.304250
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 h_monomial.e_f.h.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.304250
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)
exacts [rfl, (zero_smul R _).symm]