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))
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))
conv_lhs =>
  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
⊢ prod (map (fun x => X + ↑C (-x)) s) = prod (map (fun r => X + ↑C r) (map (fun t => -t) s))

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)
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))
convert prod_X_add_C_eq_sum_esymm (map (fun t => -t) s) using 1
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)
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))
rw [map_map]
no goals
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)
rfl
no goals
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)
simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one]