awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
have rw₂ : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
    ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
Tactic: rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
have rw₃ : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
    ∑ x ∈ powersetCard k univ, HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∏ i ∈ x, X i
Tactic: rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
rw₃ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∏ i ∈ x, X i
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
have rw₄ : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
  HPow.hPow (α := MvPolynomial σ R) (-1) k *
    (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
Tactic: rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
rw₃ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∏ i ∈ x, X i
rw₄ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
have rw₅ : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
  HPow.hPow (α := MvPolynomial σ R) (-1) k * (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R)) *
    ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
Tactic: rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
rw₃ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∏ i ∈ x, X i
rw₄ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
rw₅ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R)) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
have rw₆ : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
  HPow.hPow (α := MvPolynomial σ R) (-1) k * HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) *
    ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
Tactic: rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
rw₃ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∏ i ∈ x, X i
rw₄ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
rw₅ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R)) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₆ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
have rw₇ : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + k) * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
Tactic: rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
rw₃ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∏ i ∈ x, X i
rw₄ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
rw₅ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R)) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₆ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₇ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + k) * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
have rw₈ : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
  HMul.hMul (α := MvPolynomial σ R) 1 (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
Tactic: rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
rw₂ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ x, X i
rw₃ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      ∑ x ∈ powersetCard k univ, HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∏ i ∈ x, X i
rw₄ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k *
      (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
rw₅ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * (HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R)) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₆ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * HPow.hPow (α := MvPolynomial σ R) (-1) k * (↑k : MvPolynomial σ R) *
      ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₇ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + k) * (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
rw₈ :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
    HMul.hMul (α := MvPolynomial σ R) 1 (↑k : MvPolynomial σ R) * ∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) k * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
have rw₉ : HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i) =
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (∑ i ∈ powersetCard k univ, ∏ i ∈ i, X i)
Tactic: rw [esymm, sum_filter_pairs_eq_sum_powersetCard_sum σ R k (fun t ↦ weight σ R k t),
    sum_congr rfl (esymm_summand_to_weight σ R k), mul_comm (k : MvPolynomial σ R) ((-1) ^ k),
    ← mul_sum, ← mul_assoc, ← mul_assoc, ← pow_add, Even.neg_one_pow ⟨k, rfl⟩, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
⊢ ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, weight σ R k (A, j) =
    HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
have simp : Eq (α := MvPolynomial σ R)
  (∑ x ∈ powersetCard a.1 univ,
    ∑ x_1 : σ,
      (HPow.hPow (α := MvPolynomial σ R) (-1) #x * ∏ a ∈ x, X a) * HPow.hPow (α := MvPolynomial σ R) (X x_1) (k - #x))
  (∑ i : σ,
    (∑ i ∈ powersetCard a.1 univ, HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ i, X a) *
      HPow.hPow (α := MvPolynomial σ R) (X i) a.2)
Tactic: simp only [esymm, psum, weight, ← mul_assoc, mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
⊢ Eq (α := MvPolynomial σ R)
    (∑ x ∈ powersetCard a.1 univ,
      ∑ x_1 : σ,
        (HPow.hPow (α := MvPolynomial σ R) (-1) #x * ∏ a ∈ x, X a) * HPow.hPow (α := MvPolynomial σ R) (X x_1) (k - #x))
    (∑ i : σ,
      (∑ i ∈ powersetCard a.1 univ, HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ i, X a) *
        HPow.hPow (α := MvPolynomial σ R) (X i) a.2)
have rw : Eq (α := MvPolynomial σ R)
  (∑ y : σ,
    ∑ x ∈ powersetCard a.1 univ,
      (HPow.hPow (α := MvPolynomial σ R) (-1) #x * ∏ a ∈ x, X a) * HPow.hPow (α := MvPolynomial σ R) (X y) (k - #x))
  (∑ i : σ,
    (∑ i ∈ powersetCard a.1 univ, HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ i, X a) *
      HPow.hPow (α := MvPolynomial σ R) (X i) a.2)
Tactic: rw [sum_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
⊢ Eq (α := MvPolynomial σ R)
    (∑ y : σ,
      ∑ x ∈ powersetCard a.1 univ,
        (HPow.hPow (α := MvPolynomial σ R) (-1) #x * ∏ a ∈ x, X a) * HPow.hPow (α := MvPolynomial σ R) (X y) (k - #x))
    (∑ i : σ,
      (∑ i ∈ powersetCard a.1 univ, HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ i, X a) *
        HPow.hPow (α := MvPolynomial σ R) (X i) a.2)
have refine : ∀ (x : σ),
  Membership.mem (γ := Finset σ) univ x →
    ∑ x_2 ∈ powersetCard a.1 univ,
        (HPow.hPow (α := MvPolynomial σ R) (-1) #x_2 * ∏ a ∈ x_2, X a) *
          HPow.hPow (α := MvPolynomial σ R) (X x) (k - #x_2) =
      (∑ i ∈ powersetCard a.1 univ, HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ i, X a) *
        HPow.hPow (α := MvPolynomial σ R) (X x) a.2
Tactic: refine sum_congr rfl fun x _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
x : σ
h : Membership.mem (γ := Finset σ) univ x
⊢ ∑ x_1 ∈ powersetCard a.1 univ,
      (HPow.hPow (α := MvPolynomial σ R) (-1) #x_1 * ∏ a ∈ x_1, X a) *
        HPow.hPow (α := MvPolynomial σ R) (X x) (k - #x_1) =
    (∑ i ∈ powersetCard a.1 univ, HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ i, X a) *
      HPow.hPow (α := MvPolynomial σ R) (X x) a.2
have rw : Eq (α := MvPolynomial σ R)
  (∑ x_1 ∈ powersetCard a.1 univ,
    (HPow.hPow (α := MvPolynomial σ R) (-1) #x_1 * ∏ a ∈ x_1, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) (k - #x_1))
  (∑ i ∈ powersetCard a.1 univ,
    (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ i, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) a.2)
Tactic: rw [sum_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
x : σ
h : Membership.mem (γ := Finset σ) univ x
⊢ Eq (α := MvPolynomial σ R)
    (∑ x_1 ∈ powersetCard a.1 univ,
      (HPow.hPow (α := MvPolynomial σ R) (-1) #x_1 * ∏ a ∈ x_1, X a) *
        HPow.hPow (α := MvPolynomial σ R) (X x) (k - #x_1))
    (∑ i ∈ powersetCard a.1 univ,
      (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ i, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) a.2)
have refine : ∀ (s : Finset σ) (hs : Membership.mem (γ := Finset (Finset σ)) (powersetCard a.1 univ) s),
  (HPow.hPow (α := MvPolynomial σ R) (-1) #s * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) (k - #s) =
    (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) a.2
Tactic: refine sum_congr rfl fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
x : σ
h : Membership.mem (γ := Finset σ) univ x
s : Finset σ
hs : Membership.mem (γ := Finset (Finset σ)) (powersetCard a.1 univ) s
⊢ (HPow.hPow (α := MvPolynomial σ R) (-1) #s * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) (k - #s) =
    (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) a.2
have rw : (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) (k - a.1) =
  (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) a.2
Tactic: rw [mem_powersetCard_univ.mp hs, ← mem_antidiagonal.mp ha, add_sub_self_left]