awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ = n
i : Fin n
⊢ Eq (α := ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
        ((AlgEquiv.symm (esymmAlgEquiv σ R hn) : (a : ↥(symmetricSubalgebra σ R)) → MvPolynomial (Fin n) R)
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
            (esymm σ R ((↑i : ℕ) + 1)) ⋯)) :
      ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i) : ↥(symmetricSubalgebra σ R))
have simp_rw : Eq (α := ↥(symmetricSubalgebra σ R))
  ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
      ((AlgEquiv.symm (AlgEquiv.ofBijective (esymmAlgHom σ R n) sorry) :
          (a : ↥(symmetricSubalgebra σ R)) → MvPolynomial (Fin n) R)
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1))
          sorry)) :
    ↥(symmetricSubalgebra σ R))
  ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i) : ↥(symmetricSubalgebra σ R))
Tactic: simp_rw [esymmAlgEquiv, AlgEquiv.ofBijective_apply_symm_apply, esymmAlgHom, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ = n
i : Fin n
simp_rw :
  Eq (α := ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
        ((AlgEquiv.symm (AlgEquiv.ofBijective (esymmAlgHom σ R n) ⋯) :
            (a : ↥(symmetricSubalgebra σ R)) → MvPolynomial (Fin n) R)
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
            (esymm σ R ((↑i : ℕ) + 1)) ⋯)) :
      ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i) : ↥(symmetricSubalgebra σ R))
⊢ Eq (α := ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
        ((AlgEquiv.symm (esymmAlgEquiv σ R hn) : (a : ↥(symmetricSubalgebra σ R)) → MvPolynomial (Fin n) R)
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
            (esymm σ R ((↑i : ℕ) + 1)) ⋯)) :
      ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i) : ↥(symmetricSubalgebra σ R))
have simp_rw₁ : Eq (α := ↥(symmetricSubalgebra σ R))
  (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
    Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1)) sorry)
  ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i))
Tactic: simp_rw [esymmAlgEquiv, AlgEquiv.ofBijective_apply_symm_apply, esymmAlgHom, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ = n
i : Fin n
simp_rw :
  Eq (α := ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
        ((AlgEquiv.symm (AlgEquiv.ofBijective (esymmAlgHom σ R n) ⋯) :
            (a : ↥(symmetricSubalgebra σ R)) → MvPolynomial (Fin n) R)
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
            (esymm σ R ((↑i : ℕ) + 1)) ⋯)) :
      ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i) : ↥(symmetricSubalgebra σ R))
simp_rw₁ :
  Eq (α := ↥(symmetricSubalgebra σ R))
    (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1)) ⋯)
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i))
⊢ Eq (α := ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
        ((AlgEquiv.symm (esymmAlgEquiv σ R hn) : (a : ↥(symmetricSubalgebra σ R)) → MvPolynomial (Fin n) R)
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
            (esymm σ R ((↑i : ℕ) + 1)) ⋯)) :
      ↥(symmetricSubalgebra σ R))
    ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i) : ↥(symmetricSubalgebra σ R))
have simp_rw₂ : Eq (α := ↥(symmetricSubalgebra σ R))
  (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
    Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1)) sorry)
  ((aeval fun (i : Fin n) ↦
        Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1))
          sorry :
      (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
    (X i))
Tactic: simp_rw [esymmAlgEquiv, AlgEquiv.ofBijective_apply_symm_apply, esymmAlgHom, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
⊢ (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)) ≠ t
have pos : ∀ (h1 : t.2 ∈ t.1), (t.1.erase t.2, t.2) ≠ t
Tactic: split_ifs with h1
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
pos : ∀ (h1 : t.2 ∈ t.1), (t.1.erase t.2, t.2) ≠ t
⊢ (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)) ≠ t
have neg : ∀ (h1 : t.2 ∉ t.1), (cons t.2 t.1 h1, t.2) ≠ t
Tactic: split_ifs with h1
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
ht : (t.1.erase t.2, t.2) = t
⊢ False
have h1₁ : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
Tactic: rw [← ht] at h1
Cleared hypotheses: h1, ht
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
ht : (cons t.2 t.1 h1, t.2) = t
⊢ False
have h1₁ : (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1
Tactic: rw [← ht] at h1
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
⊢ pairMap σ (pairMap σ t) = t
have rw : (if h :
      Membership.mem (γ := Finset σ) (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 then
    (erase (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
      (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
  else
    (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
      (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
  t
Tactic: rw [pairMap, pairMap]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
⊢ (if h :
        Membership.mem (γ := Finset σ) (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 then
      (erase (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t
have pos : ∀ (h1 : t.2 ∈ t.1) (h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1),
  ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
pos :
  ∀ (h1 : t.2 ∈ t.1) (h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1),
    ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t
⊢ (if h :
        Membership.mem (γ := Finset σ) (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 then
      (erase (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t
have neg : ∀ (h1 : t.2 ∈ t.1) (h2 : (t.1.erase t.2, t.2).2 ∉ (t.1.erase t.2, t.2).1),
  (cons (t.1.erase t.2, t.2).2 (t.1.erase t.2, t.2).1 sorry, (t.1.erase t.2, t.2).2) = t
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
pos :
  ∀ (h1 : t.2 ∈ t.1) (h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1),
    ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t
neg :
  ∀ (h1 : t.2 ∈ t.1) (h2 : (t.1.erase t.2, t.2).2 ∉ (t.1.erase t.2, t.2).1),
    (cons (t.1.erase t.2, t.2).2 (t.1.erase t.2, t.2).1 ⋯, (t.1.erase t.2, t.2).2) = t
⊢ (if h :
        Membership.mem (γ := Finset σ) (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 then
      (erase (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t
have pos₁ : ∀ (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 t.2 t.1 h1, t.2).1.erase (cons t.2 t.1 h1, t.2).2, (cons t.2 t.1 h1, t.2).2) = t
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
pos :
  ∀ (h1 : t.2 ∈ t.1) (h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1),
    ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t
neg :
  ∀ (h1 : t.2 ∈ t.1) (h2 : (t.1.erase t.2, t.2).2 ∉ (t.1.erase t.2, t.2).1),
    (cons (t.1.erase t.2, t.2).2 (t.1.erase t.2, t.2).1 ⋯, (t.1.erase t.2, t.2).2) = t
pos₁ :
  ∀ (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 t.2 t.1 h1, t.2).1.erase (cons t.2 t.1 h1, t.2).2, (cons t.2 t.1 h1, t.2).2) = t
⊢ (if h :
        Membership.mem (γ := Finset σ) (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 then
      (erase (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t
have neg₁ : ∀ (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 sorry, (cons t.2 t.1 h1, t.2).2) = t
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ pairs σ k
⊢ pairMap σ t ∈ pairs σ k
have 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)
Tactic: rw [mem_pairs] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
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)
have inl : ∀ (h1 : t.2 ∈ 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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)
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)
have inr : ∀ (h1 : t.2 ∉ 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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)
have 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)
Tactic: rw [pairMap_of_snd_mem_fst σ h1]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
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.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)
have h₁ : #t.1 ≤ k
Tactic: simp only [h1, implies_true, and_true] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #(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)
have inl : #t.1 ≤ k + 1 ∧ (#t.1 - 1 = k → ¬True ∧ True)
Tactic: simp only [card_erase_of_mem h1, tsub_le_iff_right, mem_erase, ne_eq, h1]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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)
have inl : #t.1 - 1 = k → ¬True ∧ True
Tactic: refine ⟨le_succ_of_le h, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
Goal:
σ : Type u_1
inst : DecidableEq σ
inst_1 : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #t.1 - 1 = k → ¬True ∧ True
have inl : ∀ (h2 : ¬(#t.1 - 1 = k → ¬True ∧ True)), False
Tactic: by_contra h2
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
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)
⊢ False
have h2₁ : #t.1 - 1 = k
Tactic: simp only [not_true_eq_false, and_true, not_forall, not_false_eq_true, exists_prop] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
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
⊢ False
have h₁ : #t.1 ≤ #t.1 - 1
Tactic: rw [← h2] at h
Cleared hypotheses: h, h2
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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
⊢ #(pairMap σ t).1 ≤ k ∧ (#(pairMap σ t).1 = k → (pairMap σ t).2 ∈ (pairMap σ t).1)
have 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)
Tactic: rw [pairMap_of_snd_notMem_fst σ h1]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (hypothesis)
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
⊢ #(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)
have h₁ : #t.1 ≤ k ∧ (#t.1 = k → False)
Tactic: simp only [h1] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities (goal)
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)
⊢ #(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)
have inr : #t.1 + 1 ≤ k
Tactic: simp only [card_cons, mem_cons, true_or, implies_true, and_true]
-- 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 ∈ pairs σ k
⊢ 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 h₁ : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
Tactic: rw [mem_pairs] at h
Cleared hypotheses: h
-- 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)
n : ℕ
⊢ -HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)
have rw : -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]
-- 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)
n : ℕ
rw : -1 * HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)
⊢ -HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)
have rw₁ : -1 * HPow.hPow (α := MvPolynomial σ R) (-1) n =
  HPow.hPow (α := MvPolynomial σ R) (-1) n * HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) 1
Tactic: rw [← neg_one_mul ((-1 : MvPolynomial σ R) ^ n), pow_add, pow_one, mul_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 : 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
⊢ -HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)
have rw₂ : -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]
-- 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)
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
⊢ -HPow.hPow (α := MvPolynomial σ R) (-1) n = HPow.hPow (α := MvPolynomial σ R) (-1) (n + 1)
have rw₃ : HPow.hPow (α := MvPolynomial σ R) (-1) n * -1 = HPow.hPow (α := MvPolynomial σ R) (-1) n * -1
Tactic: rw [← neg_one_mul ((-1 : MvPolynomial σ R) ^ n), pow_add, pow_one, mul_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)
⊢ 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 h2 : ∀ (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]
-- 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)
⊢ 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 : ∀ (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