-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem prod_X_add_C_eq_sum_esymm (s : Multiset R) :
    (s.map fun r => X + C r).prod =
      ∑ j ∈ Finset.range (Multiset.card s + 1), (C (s.esymm j) * X ^ (Multiset.card s - j))

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ ∀ x ∈ powersetCard x✝ s,
    ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s - t, t)) x =
      C x.prod * X ^ (s.card - x✝)

Tactic:
intro s ht

Result:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ∈ powersetCard x✝ s✝
⊢ ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s✝ - t, t)) s =
    C s.prod * X ^ (s✝.card - x✝)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map (fun r => X + C r) s).prod = ∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)

Tactic:
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_powersetCard] at ht
  dsimp
  rw [prod_hom' s (Polynomial.C : R →+* R[X])]
  simp [ht, map_const, prod_replicate, prod_hom', map_id', card_sub]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ (map ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s - t, t)) (powersetCard x✝ s)).sum =
    C (s.esymm x✝) * X ^ (s.card - x✝)

Tactic:
rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ ∀ x ∈ powersetCard x✝ s,
    ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s - t, t)) x =
      C x.prod * X ^ (s.card - x✝)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ (map (fun r => X) (s✝ - s)).prod * (map (⇑C) s).prod = C s.prod * X ^ (s✝.card - x✝)

Tactic:
rw [prod_hom' s (Polynomial.C : R →+* R[X])]

Result:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ (map (fun r => X) (s✝ - s)).prod * C (map (fun i => i) s).prod = C s.prod * X ^ (s✝.card - x✝)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s✝ - t, t)) s =
    C s.prod * X ^ (s✝.card - x✝)

Tactic:
dsimp

Result:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ (map (fun r => X) (s✝ - s)).prod * (map (⇑C) s).prod = C s.prod * X ^ (s✝.card - x✝)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ∀ x ∈ range (s.card + 1),
    (map ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s - t, t)) (powersetCard x s)).sum =
      C (s.esymm x) * X ^ (s.card - x)

Tactic:
intro _ _

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s.card + 1)
⊢ (map ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s - t, t)) (powersetCard x✝ s)).sum =
    C (s.esymm x✝) * X ^ (s.card - x✝)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ (map (fun r => X) (s✝ - s)).prod * C (map (fun i => i) s).prod = C s.prod * X ^ (s✝.card - x✝)

Tactic:
simp [ht, map_const, prod_replicate, prod_hom', map_id', card_sub]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map (fun r => X + C r) s).prod = ∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)

Tactic:
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 _)]

Result:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ ∀ x ∈ range (s.card + 1),
    (map ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s - t, t)) (powersetCard x s)).sum =
      C (s.esymm x) * X ^ (s.card - x)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ∈ powersetCard x✝ s✝
⊢ ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s✝ - t, t)) s =
    C s.prod * X ^ (s✝.card - x✝)

Tactic:
rw [mem_powersetCard] at ht

Result:
R : Type u_1
inst✝ : CommSemiring R
s✝ : Multiset R
x✝ : ℕ
a✝ : x✝ ∈ range (s✝.card + 1)
s : Multiset R
ht : s ≤ s✝ ∧ s.card = x✝
⊢ ((fun p => (map (fun r => X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t => (s✝ - t, t)) s =
    C s.prod * X ^ (s✝.card - x✝)