awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1
⊢ (cons (cons t.2 t.1 h1, t.2).2 (cons t.2 t.1 h1, t.2).1 ⋯, (cons t.2 t.1 h1, t.2).2) = t

Tactic:
simp at h3
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
⊢ t ∈ pairs σ k ↔ #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)

Tactic:
simp [pairs]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairs
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
rw :
  ∀ (h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)),
    #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)
⊢ pairMap σ t ∈ pairs σ k

Tactic:
rw [mem_pairs] at h ⊢

Premises used: _private.0.MvPolynomial.NewtonIdentities.mem_pairs
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
inl : ∀ (h1 : t.2 ∈ t.1), #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)
inr : ∀ (h1 : t.2 ∉ t.1), #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)

Tactic:
rcases (em (t.snd ∈ t.fst)) with h1 | h1

Premises used: Membership.mem, em, Prod.fst, Prod.snd
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
inl : #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)

Tactic:
rw [pairMap_of_snd_mem_fst σ h1]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairMap_of_snd_mem_fst
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #t.1 ≤ k

Tactic:
simp only [h1, implies_true, and_true] at h

Premises used: and_true, implies_true
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
inl : #t.1 ≤ k + 1 ∧ (#t.1 - 1 = k → ¬True ∧ True)
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)

Tactic:
simp only [card_erase_of_mem h1, tsub_le_iff_right, mem_erase, ne_eq, h1]

Premises used: Finset.card_erase_of_mem, ne_eq, tsub_le_iff_right, Finset.mem_erase
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #t.1 ≤ k + 1 ∧ (#t.1 - 1 = k → ¬True ∧ True)

Tactic:
⟨le_succ_of_le h, ?_⟩

Premises used: And.intro, Nat.le_succ_of_le
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
inl : #t.1 - 1 = k → ¬True ∧ True
⊢ #t.1 ≤ k + 1 ∧ (#t.1 - 1 = k → ¬True ∧ True)

Tactic:
refine ⟨le_succ_of_le h, ?_⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
inl : ∀ (h2 : ¬(#t.1 - 1 = k → ¬True ∧ True)), False
⊢ #t.1 - 1 = k → ¬True ∧ True

Tactic:
by_contra h2
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
h2 : ¬(#t.1 - 1 = k → ¬True ∧ True)
⊢ #t.1 - 1 = k

Tactic:
simp only [not_true_eq_false, and_true, not_forall, not_false_eq_true, exists_prop] at h2

Premises used: and_true, not_true_eq_false, exists_prop, not_false_eq_true, Classical.not_forall
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
h2 : #t.1 - 1 = k
⊢ #t.1 ≤ #t.1 - 1

Tactic:
rw [← h2] at h
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
h2 : #t.1 - 1 = k
h₁ : #t.1 ≤ #t.1 - 1
⊢ #t.1 - 1 = k

Tactic:
rw [← h2] at h
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ #t.1 - 1
h2 : #t.1 - 1 = k
⊢ False

Tactic:
not_le_of_gt (sub_lt (card_pos.mpr ⟨t.snd, h1⟩) zero_lt_one) h

Premises used: Iff.mpr, Nat.sub_lt, zero_lt_one, Exists.intro, Finset.card_pos, not_le_of_gt, Prod.snd
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ #t.1 - 1
h2 : #t.1 - 1 = k
⊢ False

Tactic:
exact not_le_of_gt (sub_lt (card_pos.mpr ⟨t.snd, h1⟩) zero_lt_one) h

Premises used: Iff.mpr, Nat.sub_lt, zero_lt_one, Exists.intro, Finset.card_pos, not_le_of_gt, Prod.snd
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
inr :
  #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)

Tactic:
rw [pairMap_of_snd_notMem_fst σ h1]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairMap_of_snd_notMem_fst
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #t.1 ≤ k ∧ (#t.1 = k → False)

Tactic:
simp only [h1] at h
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
inr : #t.1 + 1 ≤ k
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)

Tactic:
simp only [card_cons, mem_cons, true_or, implies_true, and_true]

Premises used: and_true, true_or, Finset.card_cons, implies_true, Finset.mem_cons
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
⊢ #t.1 + 1 ≤ k

Tactic:
(le_iff_eq_or_lt.mp h.left).resolve_left h.right

Premises used: le_iff_eq_or_lt, Or.resolve_left, And.right, And.left, Iff.mp, Nat.lt
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
⊢ #t.1 + 1 ≤ k

Tactic:
exact (le_iff_eq_or_lt.mp h.left).resolve_left h.right

Premises used: le_iff_eq_or_lt, Or.resolve_left, And.right, And.left, Iff.mp
-- 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 ∈ pairs σ k
⊢ #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)

Tactic:
rw [mem_pairs] at h

Premises used: _private.0.MvPolynomial.NewtonIdentities.mem_pairs
-- 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)
n : ℕ
rw : -1 * HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)
rw₁ :
  -1 * HPow.hPow (α := MvPolynomial σ R) (-1) n =
    HPow.hPow (α := MvPolynomial σ R) (-1) n * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) 1
rw₂ : -1 * HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) n * -1
rw₃ rw₄ : HPow.hPow (α := MvPolynomial σ R) (-1) n * -1 = HPow.hPow (α := MvPolynomial σ R) (-1) n * -1
⊢ -HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)

Tactic:
rw [← neg_one_mul ((-1 : MvPolynomial σ R) ^ n), pow_add, pow_one, mul_comm]

Premises used: neg_one_mul, pow_add, HPow.hPow, pow_one, mul_comm, OfNat.ofNat, Neg.neg
-- 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)
⊢ ∀ (n : ℕ), -HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)

Tactic:
have h2 (n : ℕ) : -(-1 : MvPolynomial σ R) ^ n = (-1) ^ (n + 1) := by
    rw [← neg_one_mul ((-1 : MvPolynomial σ R) ^ n), pow_add, pow_one, mul_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 : ℕ
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
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
⊢ 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

Premises used: Membership.mem, em, Prod.fst, Prod.snd
-- 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
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
⊢ 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:
rw [pairMap_of_snd_mem_fst σ h1]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairMap_of_snd_mem_fst
-- 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
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
⊢ 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:
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]

Premises used: Finset.prod_erase_mul, mul_assoc, MvPolynomial.X, Finset.card_erase_of_mem, Prod.fst, Finset.prod, Finset.erase, Prod.snd
-- 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
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
⊢ 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:
nth_rewrite 1 [← pow_one (X t.snd)]

Premises used: MvPolynomial.X, pow_one, Prod.snd
-- 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
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
⊢ 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:
simp only [← pow_add, add_comm]

Premises used: pow_add, add_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 : ℕ
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
⊢ 1 ≤ #t.1

Tactic:
have h3 : 1 ≤ #t.1 := lt_iff_add_one_le.mp (card_pos.mpr ⟨t.snd, h1⟩)
-- 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
h3 : 1 ≤ #t.1
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
⊢ 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:
rw [← tsub_tsub_assoc h.left h3, ← neg_neg ((-1 : MvPolynomial σ R) ^ (#t.1 - 1)),
      h2 (#t.1 - 1), Nat.sub_add_cancel h3]

Premises used: HSub.hSub, neg_neg, Prod.fst, Nat.sub_add_cancel, HPow.hPow, And.left, tsub_tsub_assoc, Finset.card, OfNat.ofNat, Neg.neg
-- 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
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 *
        ((∏ a ∈ t.1.erase t.2, X a) * HPow.hPow (α := MvPolynomial σ R) (X t.2) (k - (#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 : ℕ
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
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
⊢ 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:
rw [pairMap_of_snd_notMem_fst σ h1]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairMap_of_snd_notMem_fst
-- 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
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
⊢ 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:
simp only [mul_comm, mul_assoc (∏ a ∈ t.fst, X a), card_cons, prod_cons]

Premises used: mul_assoc, MvPolynomial.X, Prod.fst, Finset.prod, Finset.card_cons, Finset.prod_cons, mul_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 : ℕ
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
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
⊢ (∏ 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:
nth_rewrite 2 [← pow_one (X t.snd)]

Premises used: MvPolynomial.X, pow_one, Prod.snd
-- 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
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
⊢ (∏ 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:
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]

Premises used: Nat.succ_eq_add_one, Nat.add_sub_assoc, pow_add, mt, add_comm, And.right, And.left, Nat.lt_of_le_of_ne, Nat.add_sub_add_right
-- 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
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
⊢ (∏ 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:
rw [← neg_neg ((-1 : MvPolynomial σ R) ^ #t.1), h2]

Premises used: neg_neg, Prod.fst, HPow.hPow, Finset.card, OfNat.ofNat, Neg.neg