-- 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.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
⊢ (hd * tl.prod).coeff (hd.natDegree + hd.natDegree * tl.length) =
    hd.coeff hd.natDegree * tl.prod.coeff (hd.natDegree * tl.length)

Tactic:
rcases h.eq_or_lt with h' | h'

Result:
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)

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)

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
⊢ (hd :: tl).prod.coeff ((hd :: tl).length * n) = (List.map (fun p => p.coeff n) (hd :: tl)).prod

Tactic:
have hl' : ∀ p ∈ tl, natDegree p ≤ n := fun p hp => hl p (List.mem_cons_of_mem _ hp)

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 ((hd :: tl).length * n) = (List.map (fun p => p.coeff n) (hd :: 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
⊢ (List.map natDegree tl).sum ≤ n * tl.length

Tactic:
rw [← tl.length_map natDegree, mul_comm]

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 ≤ (List.map natDegree tl).length * n

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
hdn : hd.natDegree ≤ n
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

Tactic:
rcases hdn.eq_or_lt with (rfl | hdn')

Result:
case cons.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
⊢ (hd * tl.prod).coeff (hd.natDegree + hd.natDegree * tl.length) =
    hd.coeff hd.natDegree * tl.prod.coeff (hd.natDegree * tl.length)

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)

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

Tactic:
induction' l with hd tl IH

Result:
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

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
⊢ (hd :: tl).prod.coeff ((hd :: tl).length * n) = (List.map (fun p => p.coeff n) (hd :: tl)).prod

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).natDegree < n + n * tl.length

Tactic:
exact natDegree_mul_le.trans_lt (add_lt_add_of_lt_of_le hdn' 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 (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

Tactic:
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'

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
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

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 ((tl.length + 1) * n) = hd.coeff n * (List.map (fun p => p.coeff n) tl).prod

Tactic:
rw [add_mul, one_mul, add_comm, ← IH hl', mul_comm tl.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 (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)