Equal Power Sums Imply Equal Symmetric Functions

  intro m hm
  -- We prove by strong induction on m
  induction m using Nat.strong_induction_on with
  | h m IH =>
    by_cases hm_zero : m = 0
    · -- Base case: esymm 0 = 1 for any multiset
      rw [hm_zero]
      simp [Multiset.esymm]
    · -- Inductive case: m > 0, use Newton's identity
      have hm_pos : 0 < m := Nat.pos_of_ne_zero hm_zero
      -- Apply Newton's identity to both s and t
      have h_newton_s := multiset_newton_identity s m hm_pos
      have h_newton_t := multiset_newton_identity t m hm_pos
      -- The RHS of Newton's identity should be equal for s and t
      have h_rhs_eq : (Finset.antidiagonal m).sum (fun a =>
            if a.1 < m then (-1)^a.1 * s.esymm a.1 * (s.map (fun x => x ^ a.2)).sum
            else 0) =
          (Finset.antidiagonal m).sum (fun a =>
            if a.1 < m then (-1)^a.1 * t.esymm a.1 * (t.map (fun x => x ^ a.2)).sum
            else 0) := by
        apply Finset.sum_congr rfl
        intro a ha
        -- a ∈ antidiagonal m means a.1 + a.2 = m
        have h_sum : a.1 + a.2 = m := Finset.mem_antidiagonal.mp ha
        split_ifs with ha_lt
        · -- When a.1 < m, show the terms are equal
          congr 1
          · congr 1  -- esymm a.1 equal by IH
            have ha1_bound : a.1 < s.card := by omega
            exact IH a.1 ha_lt ha1_bound
          · -- Power sums equal by hypothesis
            by_cases ha2_zero : a.2 = 0
            · -- When a.2 = 0, both power sums are cardinalities
              simp only [ha2_zero, pow_zero]
              -- Simplify x^0 = 1, then sum of 1s equals card
              convert_to (s.card : ℝ) = (t.card : ℝ) using 1 <;>
                simp
              exact_mod_cast h_card
            · have ha2_pos : 0 < a.2 := Nat.pos_of_ne_zero ha2_zero
              have ha2_bound : a.2 < s.card := by omega
              exact h_psum a.2 ha2_pos ha2_bound
        · rfl
      -- Now use Newton's identity to extract esymm m
      have h_eq : (m : ℝ) * s.esymm m = (m : ℝ) * t.esymm m := by
        rw [h_newton_s, h_newton_t, h_rhs_eq]
      -- Cancel the factor of m
      have hm_ne_zero : (m : ℝ) ≠ 0 := by
        exact_mod_cast hm_zero
      exact mul_left_cancel₀ hm_ne_zero h_eq