[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ prod (map (fun r => X + ↑C r) s) = ∑ j in Finset.range (↑card s + 1), ↑C (esymm s j) * X ^ (↑card s - j)
[PROOFSTEP]
classical
rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len, map_bind, sum_bind,
  Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
intro _ _
rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
intro s ht
rw [mem_powersetLen] at ht 
dsimp
rw [prod_hom' s (Polynomial.C : R →+* R[X])]
simp [ht, map_const, prod_replicate, prod_hom', map_id', card_sub]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ prod (map (fun r => X + ↑C r) s) = ∑ j in Finset.range (↑card s + 1), ↑C (esymm s j) * X ^ (↑card s - j)
[PROOFSTEP]
rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len, map_bind, sum_bind,
  Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ∀ (x : ℕ),
    x ∈ range (↑card s + 1) →
      sum
          (map ((fun p => prod (map (fun r => X) p.fst) * prod (map (fun r => ↑C r) p.snd)) ∘ fun t => (s - t, t))
            (powersetLen x s)) =
        ↑C (esymm s x) * X ^ (↑card s - x)
[PROOFSTEP]
intro _ _
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (↑card s + 1)
⊢ sum
      (map ((fun p => prod (map (fun r => X) p.fst) * prod (map (fun r => ↑C r) p.snd)) ∘ fun t => (s - t, t))
        (powersetLen x✝ s)) =
    ↑C (esymm s x✝) * X ^ (↑card s - x✝)
[PROOFSTEP]
rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (↑card s + 1)
⊢ ∀ (x : Multiset R),
    x ∈ powersetLen x✝ s →
      ((fun p => prod (map (fun r => X) p.fst) * prod (map (fun r => ↑C r) p.snd)) ∘ fun t => (s - t, t)) x =
        ↑C (prod x) * X ^ (↑card s - x✝)
[PROOFSTEP]
intro s ht
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (↑card s✝ + 1)
s : Multiset R
ht : s ∈ powersetLen x✝ s✝
⊢ ((fun p => prod (map (fun r => X) p.fst) * prod (map (fun r => ↑C r) p.snd)) ∘ fun t => (s✝ - t, t)) s =
    ↑C (prod s) * X ^ (↑card s✝ - x✝)
[PROOFSTEP]
rw [mem_powersetLen] at ht 
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (↑card s✝ + 1)
s : Multiset R
ht : s ≤ s✝ ∧ ↑card s = x✝
⊢ ((fun p => prod (map (fun r => X) p.fst) * prod (map (fun r => ↑C r) p.snd)) ∘ fun t => (s✝ - t, t)) s =
    ↑C (prod s) * X ^ (↑card s✝ - x✝)
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (↑card s✝ + 1)
s : Multiset R
ht : s ≤ s✝ ∧ ↑card s = x✝
⊢ prod (map (fun r => X) (s✝ - s)) * prod (map (fun r => ↑C r) s) = ↑C (prod s) * X ^ (↑card s✝ - x✝)
[PROOFSTEP]
rw [prod_hom' s (Polynomial.C : R →+* R[X])]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (↑card s✝ + 1)
s : Multiset R
ht : s ≤ s✝ ∧ ↑card s = x✝
⊢ prod (map (fun r => X) (s✝ - s)) * ↑C (prod (map (fun r => r) s)) = ↑C (prod s) * X ^ (↑card s✝ - x✝)
[PROOFSTEP]
simp [ht, map_const, prod_replicate, prod_hom', map_id', card_sub]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ coeff (prod (map (fun r => X + ↑C r) s)) k = esymm s (↑card s - k)
[PROOFSTEP]
convert Polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k using 1
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = coeff (∑ j in Finset.range (↑card s + 1), ↑C (esymm s j) * X ^ (↑card s - j)) k
[PROOFSTEP]
simp_rw [finset_sum_coeff, coeff_C_mul_X_pow]
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = ∑ x in Finset.range (↑card s + 1), if k = ↑card s - x then esymm s x else 0
[PROOFSTEP]
rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _]
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ esymm s (↑card s - k) = if k = ↑card s - (↑card s - k) then esymm s (↑card s - k) else 0
[PROOFSTEP]
rw [if_pos (Nat.sub_sub_self h).symm]
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ∀ (b : (fun x => ℕ) s),
    b ∈ Finset.range (↑card s + 1) → b ≠ ↑card s - k → (if k = ↑card s - b then esymm s b else 0) = 0
[PROOFSTEP]
intro j hj1 hj2
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
⊢ (if k = ↑card s - j then esymm s j else 0) = 0
[PROOFSTEP]
suffices k ≠ card s - j by rw [if_neg this]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
this : k ≠ ↑card s - j
⊢ (if k = ↑card s - j then esymm s j else 0) = 0
[PROOFSTEP]
rw [if_neg this]
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
⊢ k ≠ ↑card s - j
[PROOFSTEP]
intro hn
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ ↑card s - k
hn : k = ↑card s - j
⊢ False
[PROOFSTEP]
rw [hn, Nat.sub_sub_self (Nat.lt_succ_iff.mp (Finset.mem_range.mp hj1))] at hj2 
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
j : ℕ
hj1 : j ∈ Finset.range (↑card s + 1)
hj2 : j ≠ j
hn : k = ↑card s - j
⊢ False
[PROOFSTEP]
exact Ne.irrefl hj2
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ↑card s - k ∈ Finset.range (↑card s + 1)
[PROOFSTEP]
rw [Finset.mem_range]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ↑card s - k < ↑card s + 1
[PROOFSTEP]
exact Nat.sub_lt_succ (Multiset.card s) k
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ ↑card s
⊢ coeff (prod (map (fun i => X + ↑C (r i)) s)) k = esymm (map r s) (↑card s - k)
[PROOFSTEP]
erw [← map_map (fun r => X + C r) r, prod_X_add_C_coeff]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ ↑card s
⊢ esymm (map r s) (↑card (map r s) - k) = esymm (map r s) (↑card s - k)
[PROOFSTEP]
rw [s.card_map r]
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ ↑card s
⊢ k ≤ ↑card (map r s)
[PROOFSTEP]
rw [s.card_map r]
[GOAL]
case h
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Multiset σ
r : σ → R
k : ℕ
h : k ≤ ↑card s
⊢ k ≤ ↑card s
[PROOFSTEP]
assumption
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ Finset.card s
⊢ coeff (∏ i in s, (X + ↑C (r i))) k = ∑ t in Finset.powersetLen (Finset.card s - k) s, ∏ i in t, r i
[PROOFSTEP]
rw [Finset.prod, prod_X_add_C_coeff' _ r h, Finset.esymm_map_val]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
s : Finset σ
r : σ → R
k : ℕ
h : k ≤ Finset.card s
⊢ ∑ t in Finset.powersetLen (↑card s.val - k) s, Finset.prod t r =
    ∑ t in Finset.powersetLen (Finset.card s - k) s, ∏ i in t, r i
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ esymm (map Neg.neg s) k = (-1) ^ k * esymm s k
[PROOFSTEP]
rw [esymm, esymm, ← Multiset.sum_map_mul_left, Multiset.powersetLen_map, Multiset.map_map, map_congr (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ ∀ (x : Multiset R), x ∈ powersetLen k s → (prod ∘ map Neg.neg) x = (-1) ^ k * prod x
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = (-1) ^ k * prod x
[PROOFSTEP]
rw [(mem_powersetLen.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * prod x
[PROOFSTEP]
nth_rw 3 [← map_id' x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map (Function.const R (-1)) x) * prod (map (fun x => x) x)
[PROOFSTEP]
rw [← prod_map_mul, map_congr (Eq.refl _)]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ (prod ∘ map Neg.neg) x = prod (map ?m.852287 x)
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ ∀ (x_1 : R), x_1 ∈ x → Function.const R (-1) x_1 * x_1 = ?m.852287 x_1
R : Type u_1 inst✝ : CommRing R s : Multiset R k : ℕ x : Multiset R hx : x ∈ powersetLen k s ⊢ R → R
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetLen k s
⊢ ∀ (x_1 : R), x_1 ∈ x → Function.const R (-1) x_1 * x_1 = -x_1
[PROOFSTEP]
exact fun z _ => neg_one_mul z
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ prod (map (fun t => X - ↑C t) s) = ∑ j in Finset.range (↑card s + 1), (-1) ^ j * (↑C (esymm s j) * X ^ (↑card s - j))
[PROOFSTEP]
conv_lhs =>
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| prod (map (fun t => X - ↑C t) s)
[PROOFSTEP]
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| prod (map (fun t => X - ↑C t) s)
[PROOFSTEP]
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| prod (map (fun t => X - ↑C t) s)
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| map (fun t => X - ↑C t) s
[PROOFSTEP]
congr
[GOAL]
case a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| fun t => X - ↑C t
case a.s R : Type u_1 inst✝ : CommRing R s : Multiset R | s
[PROOFSTEP]
ext x
[GOAL]
case a.f.h
R : Type u_1
inst✝ : CommRing R
s : Multiset R
x : R
| X - ↑C x
case a.s R : Type u_1 inst✝ : CommRing R s : Multiset R | s
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
case a.f.h
R : Type u_1
inst✝ : CommRing R
s : Multiset R
x : R
| X + -↑C x
case a.s R : Type u_1 inst✝ : CommRing R s : Multiset R | s
[PROOFSTEP]
rw [← map_neg C x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ prod (map (fun x => X + ↑C (-x)) s) =
    ∑ j in Finset.range (↑card s + 1), (-1) ^ j * (↑C (esymm s j) * X ^ (↑card s - j))
[PROOFSTEP]
convert prod_X_add_C_eq_sum_esymm (map (fun t => -t) s) using 1
[GOAL]
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ prod (map (fun x => X + ↑C (-x)) s) = prod (map (fun r => X + ↑C r) (map (fun t => -t) s))
[PROOFSTEP]
rw [map_map]
[GOAL]
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ prod (map (fun x => X + ↑C (-x)) s) = prod (map ((fun r => X + ↑C r) ∘ fun t => -t) s)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
⊢ ∑ j in Finset.range (↑card s + 1), (-1) ^ j * (↑C (esymm s j) * X ^ (↑card s - j)) =
    ∑ j in Finset.range (↑card (map (fun t => -t) s) + 1),
      ↑C (esymm (map (fun t => -t) s) j) * X ^ (↑card (map (fun t => -t) s) - j)
[PROOFSTEP]
simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ coeff (prod (map (fun t => X - ↑C t) s)) k = (-1) ^ (↑card s - k) * esymm s (↑card s - k)
[PROOFSTEP]
conv_lhs =>
  congr
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| coeff (prod (map (fun t => X - ↑C t) s)) k
[PROOFSTEP]
  congr
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| coeff (prod (map (fun t => X - ↑C t) s)) k
[PROOFSTEP]
  congr
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| coeff (prod (map (fun t => X - ↑C t) s)) k
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| prod (map (fun t => X - ↑C t) s)
case a R : Type u_1 inst✝ : CommRing R s : Multiset R k : ℕ h : k ≤ ↑card s | k
[PROOFSTEP]
congr
[GOAL]
case a.a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| map (fun t => X - ↑C t) s
case a R : Type u_1 inst✝ : CommRing R s : Multiset R k : ℕ h : k ≤ ↑card s | k
[PROOFSTEP]
congr
[GOAL]
case a.a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| fun t => X - ↑C t
case a.a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| s
case a R : Type u_1 inst✝ : CommRing R s : Multiset R k : ℕ h : k ≤ ↑card s | k
[PROOFSTEP]
ext x
[GOAL]
case a.a.f.h
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
x : R
| X - ↑C x
case a.a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| s
case a R : Type u_1 inst✝ : CommRing R s : Multiset R k : ℕ h : k ≤ ↑card s | k
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
case a.a.f.h
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
x : R
| X + -↑C x
case a.a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
| s
case a R : Type u_1 inst✝ : CommRing R s : Multiset R k : ℕ h : k ≤ ↑card s | k
[PROOFSTEP]
rw [← map_neg C x]
[GOAL]
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ coeff (prod (map (fun x => X + ↑C (-x)) s)) k = (-1) ^ (↑card s - k) * esymm s (↑card s - k)
[PROOFSTEP]
convert prod_X_add_C_coeff (map (fun t => -t) s) _ using 1
[GOAL]
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ coeff (prod (map (fun x => X + ↑C (-x)) s)) k =
    coeff (prod (map (fun r => X + ↑C r) (map (fun t => -t) s))) ?convert_1
[PROOFSTEP]
rw [map_map]
[GOAL]
case h.e'_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ coeff (prod (map (fun x => X + ↑C (-x)) s)) k = coeff (prod (map ((fun r => X + ↑C r) ∘ fun t => -t) s)) ?convert_1
case convert_1 R : Type u_1 inst✝ : CommRing R s : Multiset R k : ℕ h : k ≤ ↑card s ⊢ ℕ
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ (-1) ^ (↑card s - k) * esymm s (↑card s - k) = esymm (map (fun t => -t) s) (↑card (map (fun t => -t) s) - k)
[PROOFSTEP]
rw [esymm_neg, card_map]
[GOAL]
case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ k ≤ ↑card (map (fun t => -t) s)
[PROOFSTEP]
rwa [card_map]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
⊢ coeff p k = leadingCoeff p * (-1) ^ (natDegree p - k) * esymm (roots p) (natDegree p - k)
[PROOFSTEP]
conv_lhs => rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
| coeff p k
[PROOFSTEP]
rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
| coeff p k
[PROOFSTEP]
rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
| coeff p k
[PROOFSTEP]
rw [← C_leadingCoeff_mul_prod_multiset_X_sub_C hroots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
⊢ coeff (↑C (leadingCoeff p) * prod (map (fun a => X - ↑C a) (roots p))) k =
    leadingCoeff p * (-1) ^ (natDegree p - k) * esymm (roots p) (natDegree p - k)
[PROOFSTEP]
rw [coeff_C_mul, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
⊢ leadingCoeff p * coeff (prod (map (fun a => X - ↑C a) (roots p))) k =
    leadingCoeff p * ((-1) ^ (natDegree p - k) * esymm (roots p) (natDegree p - k))
[PROOFSTEP]
congr
[GOAL]
case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
⊢ coeff (prod (map (fun a => X - ↑C a) (roots p))) k = (-1) ^ (natDegree p - k) * esymm (roots p) (natDegree p - k)
[PROOFSTEP]
have : k ≤ card (roots p) := by rw [hroots]; exact h
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
⊢ k ≤ ↑card (roots p)
[PROOFSTEP]
rw [hroots]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
⊢ k ≤ natDegree p
[PROOFSTEP]
exact h
[GOAL]
case e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
this : k ≤ ↑card (roots p)
⊢ coeff (prod (map (fun a => X - ↑C a) (roots p))) k = (-1) ^ (natDegree p - k) * esymm (roots p) (natDegree p - k)
[PROOFSTEP]
convert p.roots.prod_X_sub_C_coeff this using 3
[GOAL]
case h.e'_3.h.e'_5.h.e'_6
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
this : k ≤ ↑card (roots p)
⊢ natDegree p - k = ↑card (roots p) - k
[PROOFSTEP]
rw [hroots]
[GOAL]
case h.e'_3.h.e'_6.h.e'_4
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : ↑card (roots p) = natDegree p
k : ℕ
h : k ≤ natDegree p
this : k ≤ ↑card (roots p)
⊢ natDegree p - k = ↑card (roots p) - k
[PROOFSTEP]
rw [hroots]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ ∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i)) =
    ∑ j in range (Fintype.card σ + 1), ↑Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
[PROOFSTEP]
let s := Finset.univ.val.map fun i : σ => (MvPolynomial.X i : MvPolynomial σ R)
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ ∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i)) =
    ∑ j in range (Fintype.card σ + 1), ↑Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
[PROOFSTEP]
have : Fintype.card σ = Multiset.card s := by rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ Fintype.card σ = ↑Multiset.card s
[PROOFSTEP]
rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ ∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i)) =
    ∑ j in range (Fintype.card σ + 1), ↑Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
[PROOFSTEP]
simp_rw [this, MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ Multiset.prod (Multiset.map (fun x => Polynomial.X + ↑Polynomial.C (X x)) univ.val) =
    ∑ x in range (↑Multiset.card (Multiset.map (fun i => X i) univ.val) + 1),
      ↑Polynomial.C (Multiset.esymm (Multiset.map X univ.val) x) *
        Polynomial.X ^ (↑Multiset.card (Multiset.map (fun i => X i) univ.val) - x)
[PROOFSTEP]
convert Multiset.prod_X_add_C_eq_sum_esymm s
[GOAL]
case h.e'_2.h.e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ Multiset.map (fun x => Polynomial.X + ↑Polynomial.C (X x)) univ.val =
    Multiset.map (fun r => Polynomial.X + ↑Polynomial.C r) s
[PROOFSTEP]
simp_rw [Multiset.map_map, Function.comp_apply]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
⊢ Polynomial.coeff (∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i))) k = esymm σ R (Fintype.card σ - k)
[PROOFSTEP]
let s := Finset.univ.val.map fun i => (MvPolynomial.X i : MvPolynomial σ R)
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ Polynomial.coeff (∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i))) k = esymm σ R (Fintype.card σ - k)
[PROOFSTEP]
have : Fintype.card σ = Multiset.card s := by rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
⊢ Fintype.card σ = ↑Multiset.card s
[PROOFSTEP]
rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
this : Fintype.card σ = ↑Multiset.card s
⊢ Polynomial.coeff (∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i))) k = esymm σ R (Fintype.card σ - k)
[PROOFSTEP]
rw [this] at h ⊢
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ ↑Multiset.card s
this : Fintype.card σ = ↑Multiset.card s
⊢ Polynomial.coeff (∏ i : σ, (Polynomial.X + ↑Polynomial.C (X i))) k = esymm σ R (↑Multiset.card s - k)
[PROOFSTEP]
rw [MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ ↑Multiset.card s
this : Fintype.card σ = ↑Multiset.card s
⊢ Polynomial.coeff (Multiset.prod (Multiset.map (fun i => Polynomial.X + ↑Polynomial.C (X i)) univ.val)) k =
    Multiset.esymm (Multiset.map X univ.val) (↑Multiset.card s - k)
[PROOFSTEP]
convert Multiset.prod_X_add_C_coeff s h
[GOAL]
case h.e'_2.h.e'_3.h.e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ ↑Multiset.card s
this : Fintype.card σ = ↑Multiset.card s
⊢ Multiset.map (fun i => Polynomial.X + ↑Polynomial.C (X i)) univ.val =
    Multiset.map (fun r => Polynomial.X + ↑Polynomial.C r) s
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_2.h.e'_3.h.e'_3
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val
h : k ≤ ↑Multiset.card s
this : Fintype.card σ = ↑Multiset.card s
⊢ Multiset.map (fun i => Polynomial.X + ↑Polynomial.C (X i)) univ.val =
    Multiset.map (fun r => Polynomial.X + ↑Polynomial.C r) (Multiset.map (fun i => X i) univ.val)
[PROOFSTEP]
simp_rw [Multiset.map_map, Function.comp_apply]
