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 : 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)
inl :
  ∀ (h1 : t.2 ∈ t.1),
    HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
          ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
        HPow.hPow (α := MvPolynomial σ R) (-1) #(pairMap σ t).1 *
          ((∏ a ∈ (pairMap σ t).1, X a) *
            HPow.hPow (α := MvPolynomial σ R) (X (pairMap σ t).2) (k - #(pairMap σ t).1)) =
      0
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
      HPow.hPow (α := MvPolynomial σ R) (-1) #(pairMap σ t).1 *
        ((∏ a ∈ (pairMap σ t).1, X a) * HPow.hPow (α := MvPolynomial σ R) (X (pairMap σ t).2) (k - #(pairMap σ t).1)) =
    0
have inr : ∀ (h1 : t.2 ∉ t.1),
  HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
      HPow.hPow (α := MvPolynomial σ R) (-1) #(pairMap σ t).1 *
        ((∏ a ∈ (pairMap σ t).1, X a) * HPow.hPow (α := MvPolynomial σ R) (X (pairMap σ t).2) (k - #(pairMap σ t).1)) =
    0
Tactic: rcases (em (t.snd ∈ t.fst)) with h1 | h1
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
      HPow.hPow (α := MvPolynomial σ R) (-1) #(pairMap σ t).1 *
        ((∏ a ∈ (pairMap σ t).1, X a) * HPow.hPow (α := MvPolynomial σ R) (X (pairMap σ t).2) (k - #(pairMap σ t).1)) =
    0
have inl : HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
      ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
    HPow.hPow (α := MvPolynomial σ R) (-1) #(t.1.erase t.2, t.2).1 *
      ((∏ a ∈ (t.1.erase t.2, t.2).1, X a) *
        HPow.hPow (α := MvPolynomial σ R) (X (t.1.erase t.2, t.2).2) (k - #(t.1.erase t.2, t.2).1)) =
  0
Tactic: rw [pairMap_of_snd_mem_fst σ h1]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
      HPow.hPow (α := MvPolynomial σ R) (-1) #(t.1.erase t.2, t.2).1 *
        ((∏ a ∈ (t.1.erase t.2, t.2).1, X a) *
          HPow.hPow (α := MvPolynomial σ R) (X (t.1.erase t.2, t.2).2) (k - #(t.1.erase t.2, t.2).1)) =
    0
have inl : HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
      ((∏ a ∈ t.1.erase t.2, X a) * (X t.2 * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1))) +
    HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 - 1) *
      ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) =
  0
Tactic: simp only [← prod_erase_mul t.fst (fun j ↦ (X j : MvPolynomial σ R)) h1,
      mul_assoc (∏ a ∈ erase t.fst t.snd, X a), card_erase_of_mem h1]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1.erase t.2, X a) * (X t.2 * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1))) +
      HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 - 1) *
        ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) =
    0
have inl : HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
      ((∏ a ∈ t.1.erase t.2, X a) *
        (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X t.2) 1 * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1))) +
    HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 - 1) *
      ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) =
  0
Tactic: nth_rewrite 1 [← pow_one (X t.snd)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1.erase t.2, X a) *
          (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X t.2) 1 *
            HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1))) +
      HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 - 1) *
        ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) =
    0
have inl : HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
      ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1 + 1)) +
    HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 - 1) *
      ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) =
  0
Tactic: simp only [← pow_add, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
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
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1 + 1)) +
      HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 - 1) *
        ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) =
    0
have h3 : 1 ≤ #t.1
Tactic: have h3 : 1 ≤ #t.1 := lt_iff_add_one_le.mp (card_pos.mpr ⟨t.snd, h1⟩)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
h3 : 1 ≤ #t.1
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1 + 1)) +
      HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 - 1) *
        ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) =
    0
have inl : HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
      ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) +
    -HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
      ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 - 1))) =
  0
Tactic: rw [← tsub_tsub_assoc h.left h3, ← neg_neg ((-1 : MvPolynomial σ R) ^ (#t.1 - 1)),
      h2 (#t.1 - 1), Nat.sub_add_cancel h3]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
      HPow.hPow (α := MvPolynomial σ R) (-1) #(pairMap σ t).1 *
        ((∏ a ∈ (pairMap σ t).1, X a) * HPow.hPow (α := MvPolynomial σ R) (X (pairMap σ t).2) (k - #(pairMap σ t).1)) =
    0
have inr : HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
      ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
    HPow.hPow (α := MvPolynomial σ R) (-1) #(cons t.2 t.1 h1, t.2).1 *
      ((∏ a ∈ (cons t.2 t.1 h1, t.2).1, X a) *
        HPow.hPow (α := MvPolynomial σ R) (X (cons t.2 t.1 h1, t.2).2) (k - #(cons t.2 t.1 h1, t.2).1)) =
  0
Tactic: rw [pairMap_of_snd_notMem_fst σ h1]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) #t.1 *
        ((∏ a ∈ t.1, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1)) +
      HPow.hPow (α := MvPolynomial σ R) (-1) #(cons t.2 t.1 h1, t.2).1 *
        ((∏ a ∈ (cons t.2 t.1 h1, t.2).1, X a) *
          HPow.hPow (α := MvPolynomial σ R) (X (cons t.2 t.1 h1, t.2).2) (k - #(cons t.2 t.1 h1, t.2).1)) =
    0
have inr : (∏ a ∈ t.1, X a) *
      (HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1) * HPow.hPow (α := MvPolynomial σ R) (-1) #t.1) +
    (∏ a ∈ t.1, X a) *
      (X t.2 * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 + 1)) *
        HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 + 1)) =
  0
Tactic: simp only [mul_comm, mul_assoc (∏ a ∈ t.fst, X a), card_cons, prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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) +
      (∏ a ∈ t.1, X a) *
        (X t.2 * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 + 1)) *
          HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 + 1)) =
    0
have inr : (∏ a ∈ t.1, X a) *
      (HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1) * HPow.hPow (α := MvPolynomial σ R) (-1) #t.1) +
    (∏ a ∈ t.1, X a) *
      (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X t.2) 1 *
          HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 + 1)) *
        HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 + 1)) =
  0
Tactic: nth_rewrite 2 [← pow_one (X t.snd)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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) +
      (∏ a ∈ t.1, X a) *
        (HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (X t.2) 1 *
            HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#t.1 + 1)) *
          HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 + 1)) =
    0
have inr : (∏ a ∈ t.1, X a) *
      (HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1) * HPow.hPow (α := MvPolynomial σ R) (-1) #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)) =
  0
Tactic: simp only [← pow_add, ← Nat.add_sub_assoc (Nat.lt_of_le_of_ne h.left (mt h.right h1)), add_comm,
      Nat.succ_eq_add_one, Nat.add_sub_add_right]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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) +
      (∏ a ∈ t.1, X a) *
        (HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - #t.1) * HPow.hPow (α := MvPolynomial σ R) (-1) (#t.1 + 1)) =
    0
have inr : (∏ 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: rw [← neg_neg ((-1 : MvPolynomial σ R) ^ #t.1), h2]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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) (∑ t ∈ pairs σ k with #t.1 = k, f t) (∑ A ∈ powersetCard k univ, ∑ j ∈ A, f (A, j))
have h : ∀ (p : Finset σ × σ),
  p ∈ {t ∈ pairs σ k | #t.1 = k} ↔ Membership.mem (γ := Finset (Finset σ)) (powersetCard k univ) p.1 ∧ p.2 ∈ p.1
Tactic: apply sum_finset_product
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ Eq (α := MvPolynomial σ R) (∑ t ∈ pairs σ k with #t.1 = a.1, f t) (∑ A ∈ powersetCard a.1 univ, ∑ j : σ, f (A, j))
have 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
Tactic: apply sum_finset_product
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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 σ × σ),
    p ∈ {t ∈ pairs σ k | #t.1 = a.1} ↔
      Membership.mem (γ := Finset (Finset σ)) (powersetCard a.1 univ) p.1 ∧ Membership.mem (γ := Finset σ) univ p.2
have h : ∀ (p : Finset σ × σ), #p.1 = a.1 → p ∈ pairs σ k
Tactic: simp only [mem_filter, mem_powersetCard_univ, mem_univ, and_true, and_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
have hab : #p.1 < k
Tactic: apply le_of_lt
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
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 ∈ pairs σ k
have this : #p.1 ≤ k
Tactic: have : #p.fst ≤ k := by apply le_of_lt; simp_all
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
⊢ {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
have 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) sorry)
        univ
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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) (∑ 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))
have 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))
Tactic: rw [filter_pairs_lt, sum_product, sum_disjiUnion]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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))
have refine_1 : ∀ a ∈ range k, (fun (n : ℕ) ↦ (n, k - n)) a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}
Tactic: refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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}
⊢ 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))
have refine_2 : ∀ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}, a.1 ∈ range k
Tactic: refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ 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))
have refine_3 : ∀ a ∈ range k, ((fun (n : ℕ) ↦ (n, k - n)) a).1 = a
Tactic: refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ 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))
have refine_4 : ∀ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k}, (fun (n : ℕ) ↦ (n, k - n)) a.1 = a
Tactic: refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ 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))
have 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))
Tactic: refine sum_nbij' (fun n ↦ (n, k - n)) Prod.fst ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
⊢ Disjoint ({t ∈ pairs σ k | #t.1 < k}) ({t ∈ pairs σ k | #t.1 = k})
have rw : ∀ x ∈ pairs σ k, #x.1 < k → ¬#x.1 = k
Tactic: rw [disjoint_filter]
-- 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 : ℕ
⊢ 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 * ∑ t ∈ pairs σ k with #t.1 = k, weight σ R k t
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
⊢ 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 * ∑ A ∈ powersetCard k univ, ∑ j ∈ A, weight σ R k (A, j)
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]