case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ coeff (∏ i in { val := l, nodup := hl }, f i) (Finset.card { val := l, nodup := hl } * n) =
    ∏ i in { val := l, nodup := hl }, coeff (f i) n
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
h : ∀ (p : ι), p ∈ s → natDegree (f p) ≤ n
⊢ coeff (∏ i in s, f i) (Finset.card s * n) = ∏ i in s, coeff (f i) n
cases' s with l hl
case h.e'_2.h.e'_4.h.e'_5
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ Finset.card { val := l, nodup := hl } = ↑Multiset.card (Multiset.map f l)

case h.e'_3
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ ∏ i in { val := l, nodup := hl }, coeff (f i) n = prod (Multiset.map (fun p => coeff p n) (Multiset.map f l))

case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ ∀ (p : R[X]), p ∈ Multiset.map f l → natDegree p ≤ n
case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ coeff (∏ i in { val := l, nodup := hl }, f i) (Finset.card { val := l, nodup := hl } * n) =
    ∏ i in { val := l, nodup := hl }, coeff (f i) n
convert coeff_multiset_prod_of_natDegree_le (l.map f) n ?_
no goals
case h.e'_2.h.e'_4.h.e'_5
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ Finset.card { val := l, nodup := hl } = ↑Multiset.card (Multiset.map f l)
simp
no goals
case h.e'_3
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ ∏ i in { val := l, nodup := hl }, coeff (f i) n = prod (Multiset.map (fun p => coeff p n) (Multiset.map f l))
simp
no goals
case mk
R : Type u
ι : Type w
inst✝ : CommSemiring R
f✝ : ι → R[X]
t : Multiset R[X]
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : Nodup l
h : ∀ (p : ι), p ∈ { val := l, nodup := hl } → natDegree (f p) ≤ n
⊢ ∀ (p : R[X]), p ∈ Multiset.map f l → natDegree p ≤ n
simpa using h