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)
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)
conv_lhs =>
  congr
  congr
  congr
  ext x
  rw [sub_eq_add_neg]
  rw [← map_neg C x]
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

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) - ?convert_1)

case convert_1
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ℕ

case convert_2
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ ↑card s
⊢ ?convert_1 ≤ ↑card (map (fun t => -t) s)
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)
convert prod_X_add_C_coeff (map (fun t => -t) s) _ using 1
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
⊢ ℕ
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
rw [map_map]
no goals
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
⊢ ℕ
rfl
no goals
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)
rw [esymm_neg, card_map]
no goals
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)
rwa [card_map]