awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) *
        (HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1) * -HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 + 1)) +
      (∏ a ∈ t.1, X a) *
        (HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1) * HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 + 1)) =
    0

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
⊢ Eq (α := MvPolynomial σ R) (∑ t ∈ pairs σ k, weight σ R k t) 0

Tactic:
sum_involution (fun t _ ↦ pairMap σ t) (weight_add_weight_pairMap σ R)
    (fun t _ ↦ (fun _ ↦ pairMap_ne_self σ t)) (pairMap_mem_pairs σ)
    (fun t _ ↦ pairMap_involutive σ t)

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairMap, _private.0.MvPolynomial.NewtonIdentities.pairMap_mem_pairs, _private.0.MvPolynomial.NewtonIdentities.pairMap_involutive, Finset.sum_involution, _private.0.MvPolynomial.NewtonIdentities.weight_add_weight_pairMap, _private.0.MvPolynomial.NewtonIdentities.pairMap_ne_self
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
h :
  ∀ (p : Finset σ × σ),
    p ∈ {t ∈ pairs σ k | #t.1 = k} ↔ Membership.mem (γ := Finset (Finset σ)) (powersetCard k univ) p.1 ∧ p.2 ∈ p.1
⊢ Eq (α := MvPolynomial σ R) (∑ t ∈ pairs σ k with #t.1 = k, f t) (∑ A ∈ powersetCard k univ, ∑ j ∈ A, f (A, j))

Tactic:
apply sum_finset_product

Premises used: Finset.sum_finset_product
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ (p : Finset σ × σ),
    p ∈ {t ∈ pairs σ k | #t.1 = k} ↔ Membership.mem (γ := Finset (Finset σ)) (powersetCard k univ) p.1 ∧ p.2 ∈ p.1

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
h :
  ∀ (p : Finset σ × σ),
    p ∈ {t ∈ pairs σ k | #t.1 = a.1} ↔
      Membership.mem (γ := Finset (Finset σ)) (powersetCard a.1 univ) p.1 ∧ Membership.mem (γ := Finset σ) univ p.2
⊢ Eq (α := MvPolynomial σ R) (∑ t ∈ pairs σ k with #t.1 = a.1, f t) (∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j))

Tactic:
apply sum_finset_product

Premises used: Finset.sum_finset_product
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
h : ∀ (p : Finset σ × σ), #p.1 = a.1 → p ∈ pairs σ k
⊢ ∀ (p : Finset σ × σ),
    p ∈ {t ∈ pairs σ k | #t.1 = a.1} ↔
      Membership.mem (γ := Finset (Finset σ)) (powersetCard a.1 univ) p.1 ∧ Membership.mem (γ := Finset σ) univ p.2

Tactic:
simp only [mem_filter, mem_powersetCard_univ, mem_univ, and_true, and_iff_right_iff_imp]

Premises used: Finset.mem_univ, and_true, and_iff_right_iff_imp, Finset.mem_powersetCard_univ, Finset.mem_filter
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
p : Finset σ × σ
hp : #p.1 = a.1
hab : #p.1 < k
⊢ #p.1 ≤ k

Tactic:
apply le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
p : Finset σ × σ
hp : #p.1 = a.1
⊢ #p.1 < k

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
p : Finset σ × σ
hp : #p.1 = a.1
⊢ #p.1 ≤ k

Tactic:
have : #p.fst ≤ k := by apply le_of_lt; simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
p : Finset σ × σ
hp : #p.1 = a.1
this : #p.1 ≤ k
⊢ p ∈ pairs σ k

Tactic:
aesop
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
h :
  ∀ (a : Finset σ × σ),
    a ∈
        {x ∈ pairs σ k |
          match (motive := Finset σ × σ → Prop) x with
          | (s, snd) => #s < k} ↔
      a ∈
        SProd.sprod (α := Finset (Finset σ)) (β := Finset σ)
          ((range k).disjiUnion (fun (x : ℕ) ↦ powersetCard x univ) ⋯) univ
⊢ {x ∈ pairs σ k |
      match (motive := Finset σ × σ → Prop) x with
      | (s, snd) => #s < k} =
    SProd.sprod (α := Finset (Finset σ)) (β := Finset σ) ((range k).disjiUnion (fun (x : ℕ) ↦ powersetCard x univ) ⋯)
      univ

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
a : Finset σ × σ
⊢ a ∈
      {x ∈ pairs σ k |
        match (motive := Finset σ × σ → Prop) x with
        | (s, snd) => #s < k} ↔
    a ∈
      SProd.sprod (α := Finset (Finset σ)) (β := Finset σ) ((range k).disjiUnion (fun (x : ℕ) ↦ powersetCard x univ) ⋯)
        univ

Tactic:
aesop (add unsafe le_of_lt)

Premises used: le_of_lt
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
rw :
  Eq (α := MvPolynomial σ R) (∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y : σ, f (x, y))
    (∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j))
⊢ Eq (α := MvPolynomial σ R) (∑ t ∈ pairs σ k with #t.1 < k, f t)
    (∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j))

Tactic:
rw [filter_pairs_lt, sum_product, sum_disjiUnion]

Premises used: _private.0.MvPolynomial.NewtonIdentities.filter_pairs_lt, Finset.sum_product, Finset.sum_disjiUnion
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ Eq (α := MvPolynomial σ R) (∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y : σ, f (x, y))
    (∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j))

Tactic:
sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_

Premises used: HSub.hSub, Prod.mk, Prod.fst, Finset.sum_nbij'
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
refine_1 : ∀ a ∈ range k, (fun (n : ℕ) ↦ (n, k - n)) a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}
refine_2 : ∀ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}, a.1 ∈ range k
refine_3 : ∀ a ∈ range k, ((fun (n : ℕ) ↦ (n, k - n)) a).1 = a
refine_4 : ∀ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}, (fun (n : ℕ) ↦ (n, k - n)) a.1 = a
refine_5 :
  ∀ a ∈ range k,
    Eq (α := MvPolynomial σ R) (∑ x ∈ powersetCard a univ, ∑ y : σ, f (x, y))
      (∑ A ∈ powersetCard ((fun (n : ℕ) ↦ (n, k - n)) a).1 univ, ∑ j : σ, f (A, j))
⊢ Eq (α := MvPolynomial σ R) (∑ i ∈ range k, ∑ x ∈ powersetCard i univ, ∑ y : σ, f (x, y))
    (∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j))

Tactic:
refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_

Premises used: HSub.hSub, Prod.mk, Prod.fst, Finset.sum_nbij'
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, (fun (n : ℕ) ↦ (n, k - n)) a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

Premises used: le_of_lt, eq_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}, a.1 ∈ range k

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

Premises used: le_of_lt, eq_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k, ((fun (n : ℕ) ↦ (n, k - n)) a).1 = a

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

Premises used: le_of_lt, eq_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}, (fun (n : ℕ) ↦ (n, k - n)) a.1 = a

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

Premises used: le_of_lt, eq_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq σ
inst_2 : Fintype σ
k : ℕ
f : Finset σ × σ → MvPolynomial σ R
⊢ ∀ a ∈ range k,
    Eq (α := MvPolynomial σ R) (∑ x ∈ powersetCard a univ, ∑ y : σ, f (x, y))
      (∑ A ∈ powersetCard ((fun (n : ℕ) ↦ (n, k - n)) a).1 univ, ∑ j : σ, f (A, j))

Tactic:
simp +contextual [@eq_comm _ _ k, le_of_lt]

Premises used: le_of_lt, eq_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
rw : ∀ x ∈ pairs σ k, #x.1 < k → ¬#x.1 = k
⊢ Disjoint ({t ∈ pairs σ k | #t.1 < k}) ({t ∈ pairs σ k | #t.1 = k})

Tactic:
rw [disjoint_filter]

Premises used: Finset.disjoint_filter
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
⊢ ∀ x ∈ pairs σ k, #x.1 < k → ¬#x.1 = k

Tactic:
fun _ _ h1 h2 ↦ lt_irrefl _ (h2.symm.subst h1)

Premises used: lt_irrefl, Eq.subst, Prod.fst, Finset.card, Eq.symm, Not
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
⊢ ∀ x ∈ pairs σ k, #x.1 < k → ¬#x.1 = k

Tactic:
exact fun _ _ h1 h2 ↦ lt_irrefl _ (h2.symm.subst h1)

Premises used: lt_irrefl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
⊢ {t ∈ pairs σ k | #t.1 < k}.disjUnion ({t ∈ pairs σ k | #t.1 = k}) ⋯ = pairs σ k

Tactic:
grind [MvPolynomial.NewtonIdentities.pairs]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairs
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
A : Finset σ
h : Membership.mem (γ := Finset (Finset σ)) (powersetCard k univ) A
⊢ ∑ j ∈ A, weight σ R k (A, j) = (↑k : MvPolynomial σ R) * HPow.hPow (α := MvPolynomial σ R) (-1) k * ∏ i ∈ A, X i

Tactic:
simp [weight, mem_powersetCard_univ.mp h, mul_assoc]

Premises used: mul_assoc, Finset.mem_powersetCard_univ, Iff.mp, _private.0.MvPolynomial.NewtonIdentities.weight
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
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)
⊢ ∑ 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

Tactic:
simp only [esymm, psum, weight, ← mul_assoc, mul_sum]

Premises used: Finset.mul_sum, mul_assoc, MvPolynomial.esymm, MvPolynomial.psum, _private.0.MvPolynomial.NewtonIdentities.weight
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
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)
⊢ 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:
rw [sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
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)

Tactic:
sum_congr rfl fun x _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ @antidiagonal _ instAddMonoid _ k
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
⊢ 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:
refine sum_congr rfl fun x _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
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
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)
⊢ ∑ 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]

Premises used: Finset.sum_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
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)

Tactic:
sum_congr rfl fun s hs ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
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
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
⊢ 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:
refine sum_congr rfl fun s hs ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
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
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
rw₁ :
  (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ s, X a) *
      HPow.hPow (α := MvPolynomial σ R) (X x) (a.1 + a.2 - a.1) =
    (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) a.2
rw₂ rw₃ :
  (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) a.2 =
    (HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * ∏ a ∈ s, X a) * HPow.hPow (α := MvPolynomial σ R) (X x) a.2
⊢ (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:
rw [mem_powersetCard_univ.mp hs, ← mem_antidiagonal.mp ha, add_sub_self_left]

Premises used: Nat.add_sub_self_left, Finset.HasAntidiagonal.mem_antidiagonal, Finset.mem_powersetCard_univ, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
k : ℕ
rw :
  Eq (α := MvPolynomial σ R)
    (∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, weight σ R k (A, j))
    (∑ t ∈ pairs σ k with #t.1 < k, weight σ R k t)
rw₁ rw₂ :
  Eq (α := MvPolynomial σ R)
    (∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, weight σ R k (A, j))
    (∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k, ∑ A ∈ powersetCard a.1 univ, ∑ j : σ, weight σ R k (A, j))
⊢ Eq (α := MvPolynomial σ R)
    (∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2)
    (∑ t ∈ pairs σ k with #t.1 < k, weight σ R k t)

Tactic:
rw [← sum_congr rfl (fun a ha ↦ esymm_mul_psum_summand_to_weight σ R k a (mem_filter.mp ha).left),
    sum_filter_pairs_eq_sum_filter_antidiagonal_powersetCard_sum σ R k]

Premises used: And.left, Iff.mp, Finset.mem_filter, _private.0.MvPolynomial.NewtonIdentities.sum_filter_pairs_eq_sum_filter_antidiagonal_powersetCard_sum, Finset.sum_congr, rfl, _private.0.MvPolynomial.NewtonIdentities.esymm_mul_psum_summand_to_weight
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
rw :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -1 * HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
⊢ HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2

Tactic:
rw [NewtonIdentities.esymm_to_weight σ R k, NewtonIdentities.esymm_mul_psum_to_weight σ R k,
    eq_comm, ← sub_eq_zero, sub_eq_add_neg, neg_mul_eq_neg_mul,
    neg_eq_neg_one_mul ((-1 : MvPolynomial σ R) ^ k)]

Premises used: sub_eq_zero, sub_eq_add_neg, eq_comm, _private.0.MvPolynomial.NewtonIdentities.esymm_mul_psum_to_weight, HPow.hPow, neg_eq_neg_one_mul, neg_mul_eq_neg_mul, OfNat.ofNat, _private.0.MvPolynomial.NewtonIdentities.esymm_to_weight, Neg.neg
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
nth_rw :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) 1 * HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 < k, NewtonIdentities.weight σ R k t +
      -1 * HPow.hPow (α := MvPolynomial σ R) (-1) k *
        ∑ t ∈ NewtonIdentities.pairs σ k with #t.1 = k, NewtonIdentities.weight σ R k t =
    0

Tactic:
nth_rw 2 [← pow_one (-1 : MvPolynomial σ R)]

Premises used: pow_one, OfNat.ofNat, Neg.neg