case nil
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hl : ∀ (p : S[X]), p ∈ [] → natDegree p ≤ n
⊢ coeff (List.prod []) (List.length [] * n) = List.prod (List.map (fun p => coeff p n) [])

case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
⊢ coeff (List.prod (hd :: tl)) (List.length (hd :: tl) * n) = List.prod (List.map (fun p => coeff p n) (hd :: tl))
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
⊢ coeff (List.prod l) (List.length l * n) = List.prod (List.map (fun p => coeff p n) l)
induction' l with hd tl IH
no goals
case nil
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hl : ∀ (p : S[X]), p ∈ [] → natDegree p ≤ n
⊢ coeff (List.prod []) (List.length [] * n) = List.prod (List.map (fun p => coeff p n) [])
simp
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (List.prod (hd :: tl)) (List.length (hd :: tl) * n) = List.prod (List.map (fun p => coeff p n) (hd :: tl))
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
⊢ coeff (List.prod (hd :: tl)) (List.length (hd :: tl) * n) = List.prod (List.map (fun p => coeff p n) (hd :: tl))
have hl' : ∀ p ∈ tl, natDegree p ≤ n := fun p hp => hl p (List.mem_cons_of_mem _ hp)
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (hd * List.prod tl) ((List.length tl + 1) * n) = coeff hd n * List.prod (List.map (fun p => coeff p n) tl)
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (List.prod (hd :: tl)) (List.length (hd :: tl) * n) = List.prod (List.map (fun p => coeff p n) (hd :: tl))
simp only [List.prod_cons, List.map, List.length]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (hd * List.prod tl) ((List.length tl + 1) * n) = coeff hd n * List.prod (List.map (fun p => coeff p n) tl)
rw [add_mul, one_mul, add_comm, ← IH hl', mul_comm tl.length]
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
have h : natDegree tl.prod ≤ n * tl.length := by
  refine' (natDegree_list_prod_le _).trans _
  rw [← tl.length_map natDegree, mul_comm]
  refine' List.sum_le_card_nsmul _ _ _
  simpa using hl'
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
have hdn : natDegree hd ≤ n := hl _ (List.mem_cons_self _ _)
case cons.inl
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)

case cons.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
hdn' : natDegree hd < n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
case cons
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
rcases hdn.eq_or_lt with (rfl | hdn')
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ List.sum (List.map natDegree tl) ≤ n * List.length tl
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ natDegree (List.prod tl) ≤ n * List.length tl
refine' (natDegree_list_prod_le _).trans _
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ List.sum (List.map natDegree tl) ≤ List.length (List.map natDegree tl) * n
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ List.sum (List.map natDegree tl) ≤ n * List.length tl
rw [← tl.length_map natDegree, mul_comm]
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ ∀ (x : ℕ), x ∈ List.map natDegree tl → x ≤ n
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ List.sum (List.map natDegree tl) ≤ List.length (List.map natDegree tl) * n
refine' List.sum_le_card_nsmul _ _ _
no goals
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
⊢ ∀ (x : ℕ), x ∈ List.map natDegree tl → x ≤ n
simpa using hl'
case cons.inl.inl
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) = natDegree hd * List.length tl
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)

case cons.inl.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) < natDegree hd * List.length tl
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)
case cons.inl
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)
cases' h.eq_or_lt with h' h'
no goals
case cons.inl.inl
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) = natDegree hd * List.length tl
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)
rw [← h', coeff_mul_degree_add_degree, leadingCoeff, leadingCoeff]
case cons.inl.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) < natDegree hd * List.length tl
⊢ natDegree (hd * List.prod tl) < natDegree hd + natDegree hd * List.length tl
case cons.inl.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) < natDegree hd * List.length tl
⊢ coeff (hd * List.prod tl) (natDegree hd + natDegree hd * List.length tl) =
    coeff hd (natDegree hd) * coeff (List.prod tl) (natDegree hd * List.length tl)
rw [coeff_eq_zero_of_natDegree_lt, coeff_eq_zero_of_natDegree_lt h', mul_zero]
no goals
case cons.inl.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
hd : S[X]
tl : List S[X]
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ natDegree hd
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd) →
    coeff (List.prod tl) (List.length tl * natDegree hd) = List.prod (List.map (fun p => coeff p (natDegree hd)) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ natDegree hd
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ natDegree hd
h : natDegree (List.prod tl) ≤ natDegree hd * List.length tl
hdn : natDegree hd ≤ natDegree hd
h' : natDegree (List.prod tl) < natDegree hd * List.length tl
⊢ natDegree (hd * List.prod tl) < natDegree hd + natDegree hd * List.length tl
exact natDegree_mul_le.trans_lt (add_lt_add_left h' _)
case cons.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
hdn' : natDegree hd < n
⊢ natDegree (hd * List.prod tl) < n + n * List.length tl
case cons.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
hdn' : natDegree hd < n
⊢ coeff (hd * List.prod tl) (n + n * List.length tl) = coeff hd n * coeff (List.prod tl) (n * List.length tl)
rw [coeff_eq_zero_of_natDegree_lt hdn', coeff_eq_zero_of_natDegree_lt, zero_mul]
no goals
case cons.inr
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
l : List S[X]
n : ℕ
hl✝ : ∀ (p : S[X]), p ∈ l → natDegree p ≤ n
hd : S[X]
tl : List S[X]
IH :
  (∀ (p : S[X]), p ∈ tl → natDegree p ≤ n) →
    coeff (List.prod tl) (List.length tl * n) = List.prod (List.map (fun p => coeff p n) tl)
hl : ∀ (p : S[X]), p ∈ hd :: tl → natDegree p ≤ n
hl' : ∀ (p : S[X]), p ∈ tl → natDegree p ≤ n
h : natDegree (List.prod tl) ≤ n * List.length tl
hdn : natDegree hd ≤ n
hdn' : natDegree hd < n
⊢ natDegree (hd * List.prod tl) < n + n * List.length tl
exact natDegree_mul_le.trans_lt (add_lt_add_of_lt_of_le hdn' h)