-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommSemiring R
s : Multiset R
rw :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        s.antidiagonal))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
rw₁ :
  Eq (α := R[X])
    (sum
      (map
        (fun (p : Multiset R × Multiset R) ↦
          HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2)))
        (map (fun (t : Multiset R) ↦ (s - t, t)) s.powerset)))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
rw₂ :
  Eq (α := R[X])
    (sum
      (map
        ((fun (p : Multiset R × Multiset R) ↦
            HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
          fun (t : Multiset R) ↦ (s - t, t))
        s.powerset))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
rw₃ :
  Eq.{u_1 + 1} (α := R[X])
    (sum
      (map (α := Multiset R)
        ((fun (p : Multiset R × Multiset R) ↦
            HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
          fun (t : Multiset R) ↦ (s - t, t))
        ((range (s.card + 1)).bind fun (k : ℕ) ↦ powersetCard k s)))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
rw₄ :
  Eq.{u_1 + 1} (α := R[X])
    (sum
      ((range (s.card + 1)).bind fun (a : ℕ) ↦
        map
          ((fun (p : Multiset R × Multiset R) ↦
              HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
            fun (t : Multiset R) ↦ (s - t, t))
          (powersetCard a s)))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
rw₅ :
  Eq.{u_1 + 1} (α := R[X])
    (sum
      (map
        (fun (a : ℕ) ↦
          sum
            (map
              ((fun (p : Multiset R × Multiset R) ↦
                  HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
                fun (t : Multiset R) ↦ (s - t, t))
              (powersetCard a s)))
        (range (s.card + 1))))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
rw₆ :
  Eq.{u_1 + 1} (α := R[X])
    (sum
      (map
        (fun (a : ℕ) ↦
          sum
            (map
              ((fun (p : Multiset R × Multiset R) ↦
                  HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
                fun (t : Multiset R) ↦ (s - t, t))
              (powersetCard a s)))
        (range (s.card + 1))))
    (sum
      (map
        (fun (j : ℕ) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
        (Finset.range (s.card + 1)).val))
rw₇ :
  Eq.{u_1 + 1} (α := R[X])
    (sum
      (map
        (fun (a : ℕ) ↦
          sum
            (map
              ((fun (p : Multiset R × Multiset R) ↦
                  HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
                fun (t : Multiset R) ↦ (s - t, t))
              (powersetCard a s)))
        (range (s.card + 1))))
    (sum
      (map
        (fun (j : ℕ) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
        (range (s.card + 1))))
rw₈ :
  Eq.{u_1 + 1} (α := R[X])
    (sum
      (map
        (fun (j : ℕ) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
        (range (s.card + 1))))
    (sum
      (map
        (fun (j : ℕ) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
        (range (s.card + 1))))
rw₉ :
  ∀ x ∈ range (s.card + 1),
    sum
        (map
          ((fun (p : Multiset R × Multiset R) ↦
              HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
            fun (t : Multiset R) ↦ (s - t, t))
          (powersetCard x s)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm x) : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
rw₁₀ : ℕ → R[X]
rw₁₁ :
  Eq.{u_1 + 1} (α := R[X])
    (sum
      (map
        (fun (j : ℕ) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
        (range (s.card + 1))))
    (sum
      (map
        (fun (j : ℕ) ↦
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) X (s.card - j)))
        (range (s.card + 1))))
rw₁₂ :
  ∀ x ∈ range (s.card + 1),
    sum
        (map
          ((fun (p : Multiset R × Multiset R) ↦
              HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
            fun (t : Multiset R) ↦ (s - t, t))
          (powersetCard x s)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm x) : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
rw₁₃ : ℕ → R[X]
rw₁₄ rw₁₅ :
  ∀ x ∈ range (s.card + 1),
    sum
        (map
          ((fun (p : Multiset R × Multiset R) ↦
              HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
            fun (t : Multiset R) ↦ (s - t, t))
          (powersetCard x s)) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm x) : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
rw₁₆ rw₁₇ :
  ∀ x ∈ range (s.card + 1),
    ∀ (s_1 : Multiset R) (ht : s_1 ∈ powersetCard x s),
      ((fun (p : Multiset R × Multiset R) ↦
              HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
            fun (t : Multiset R) ↦ (s - t, t))
          s_1 =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s_1.prod : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
rw₁₈ :
  ∀ x ∈ range (s.card + 1),
    ∀ (s_1 : Multiset R) (ht : s_1 ≤ s ∧ s_1.card = x),
      ((fun (p : Multiset R × Multiset R) ↦
              HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) p.1)) (prod (map (⇑C : (a : R) → R[X]) p.2))) ∘
            fun (t : Multiset R) ↦ (s - t, t))
          s_1 =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s_1.prod : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
rw₁₉ :
  ∀ x ∈ range (s.card + 1),
    ∀ (s_1 : Multiset R) (ht : s_1 ≤ s ∧ s_1.card = x),
      HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) (s - s_1))) (prod (map (⇑C : (a : R) → R[X]) s_1)) =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s_1.prod : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
rw₂₀ :
  ∀ x ∈ range (s.card + 1),
    ∀ (s_1 : Multiset R) (ht : s_1 ≤ s ∧ s_1.card = x),
      HMul.hMul (α := R[X]) (prod (map (fun (r : R) ↦ X) (s - s_1)))
          ((C : (a : R) → R[X]) (prod (map (fun (i : R) ↦ i) s_1))) =
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) s_1.prod : R[X]) (HPow.hPow (α := R[X]) X (s.card - x))
⊢ Eq (α := R[X]) (prod (map (fun (r : R) ↦ HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) s))
    (∑ j ∈ Finset.range (s.card + 1),
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (s.esymm j) : R[X]) (HPow.hPow (α := R[X]) 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, prod_replicate, map_id', card_sub]

Premises used: Finset.range_val, Multiset.prod_replicate, Polynomial.C, Multiset.mem_powersetCard, Multiset.map_bind, Multiset.antidiagonal_eq_map_powerset, Multiset.prod_map_add, Finset.sum_eq_multiset_sum, Multiset.sum_bind, Multiset.map_congr, Multiset.map_map, Multiset.esymm, Eq.refl, Multiset.map_id', Multiset.sum_map_mul_right, Multiset.sum_hom', Multiset.bind_powerset_len, Multiset.card_sub, Multiset.prod_hom'