-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Vieta (goal)
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))))
⊢ 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)))
have 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))))
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]