-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem coeff_list_prod_of_natDegree_le (l : List S[X]) (n : ℕ) (hl : ∀ p ∈ l, natDegree p ≤ n) :
    coeff (List.prod l) (l.length * n) = (l.map fun p => coeff p n).prod

Proof state:
case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
h : tl.prod.natDegree ≤ n * tl.length
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

Tactic:
have hdn : natDegree hd ≤ n := hl _ (List.mem_cons_self _ _)

Result:
case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
h : tl.prod.natDegree ≤ n * tl.length
hdn : hd.natDegree ≤ n
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

Proof state:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ tl.prod.natDegree ≤ n * tl.length

Tactic:
refine (natDegree_list_prod_le _).trans ?_

Result:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (List.map natDegree tl).sum ≤ n * tl.length

Proof state:
case cons.inl.inr
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH :
  (∀ p ∈ tl, p.natDegree ≤ hd.natDegree) →
    tl.prod.coeff (tl.length * hd.natDegree) = (List.map (fun p => p.coeff hd.natDegree) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ hd.natDegree
hl' : ∀ p ∈ tl, p.natDegree ≤ hd.natDegree
h : tl.prod.natDegree ≤ hd.natDegree * tl.length
hdn : hd.natDegree ≤ hd.natDegree
h' : tl.prod.natDegree < hd.natDegree * tl.length
⊢ (hd * tl.prod).natDegree < hd.natDegree + hd.natDegree * tl.length

Tactic:
exact natDegree_mul_le.trans_lt (add_lt_add_left h' _)

Result:
no goals

Proof state:
case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (hd :: tl).prod.coeff ((hd :: tl).length * n) = (List.map (fun p => p.coeff n) (hd :: tl)).prod

Tactic:
simp only [List.prod_cons, List.map, List.length]

Result:
case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (hd * tl.prod).coeff ((tl.length + 1) * n) = hd.coeff n * (List.map (fun p => p.coeff n) tl).prod

Proof state:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ ∀ x ∈ List.map natDegree tl, x ≤ n

Tactic:
simpa using hl'

Result:
no goals

Proof state:
case cons.inr
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
h : tl.prod.natDegree ≤ n * tl.length
hdn : hd.natDegree ≤ n
hdn' : hd.natDegree < n
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hdn', coeff_eq_zero_of_natDegree_lt, zero_mul]

Result:
case cons.inr
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
h : tl.prod.natDegree ≤ n * tl.length
hdn : hd.natDegree ≤ n
hdn' : hd.natDegree < n
⊢ (hd * tl.prod).natDegree < n + n * tl.length

Proof state:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n

Tactic:
refine List.sum_le_card_nsmul _ _ ?_

Result:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p => p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ ∀ x ∈ List.map natDegree tl, x ≤ n

Proof state:
case nil
S : Type u_1
inst✝ : Semiring S
n : ℕ
hl : ∀ p ∈ [], p.natDegree ≤ n
⊢ [].prod.coeff ([].length * n) = (List.map (fun p => p.coeff n) []).prod

Tactic:
simp

Result:
no goals

Proof state:
case cons.inl.inl
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH :
  (∀ p ∈ tl, p.natDegree ≤ hd.natDegree) →
    tl.prod.coeff (tl.length * hd.natDegree) = (List.map (fun p => p.coeff hd.natDegree) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ hd.natDegree
hl' : ∀ p ∈ tl, p.natDegree ≤ hd.natDegree
h : tl.prod.natDegree ≤ hd.natDegree * tl.length
hdn : hd.natDegree ≤ hd.natDegree
h' : tl.prod.natDegree = hd.natDegree * tl.length
⊢ (hd * tl.prod).coeff (hd.natDegree + hd.natDegree * tl.length) =
    hd.coeff hd.natDegree * tl.prod.coeff (hd.natDegree * tl.length)

Tactic:
rw [← h', coeff_mul_degree_add_degree, leadingCoeff, leadingCoeff]

Result:
no goals

Proof state:
case cons.inl.inr
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH :
  (∀ p ∈ tl, p.natDegree ≤ hd.natDegree) →
    tl.prod.coeff (tl.length * hd.natDegree) = (List.map (fun p => p.coeff hd.natDegree) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ hd.natDegree
hl' : ∀ p ∈ tl, p.natDegree ≤ hd.natDegree
h : tl.prod.natDegree ≤ hd.natDegree * tl.length
hdn : hd.natDegree ≤ hd.natDegree
h' : tl.prod.natDegree < hd.natDegree * tl.length
⊢ (hd * tl.prod).coeff (hd.natDegree + hd.natDegree * tl.length) =
    hd.coeff hd.natDegree * tl.prod.coeff (hd.natDegree * tl.length)

Tactic:
rw [coeff_eq_zero_of_natDegree_lt, coeff_eq_zero_of_natDegree_lt h', mul_zero]

Result:
case cons.inl.inr
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH :
  (∀ p ∈ tl, p.natDegree ≤ hd.natDegree) →
    tl.prod.coeff (tl.length * hd.natDegree) = (List.map (fun p => p.coeff hd.natDegree) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ hd.natDegree
hl' : ∀ p ∈ tl, p.natDegree ≤ hd.natDegree
h : tl.prod.natDegree ≤ hd.natDegree * tl.length
hdn : hd.natDegree ≤ hd.natDegree
h' : tl.prod.natDegree < hd.natDegree * tl.length
⊢ (hd * tl.prod).natDegree < hd.natDegree + hd.natDegree * tl.length