awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
hq :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R)) (AlgHom.range (esymmAlgHom (Fin m) R n))
    (HAdd.hAdd (α := ↥(symmetricSubalgebra (Fin m) R)) (β := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
        ↥(symmetricSubalgebra (Fin m) R)))

Tactic:
Subalgebra.add_mem _ hp hq

Premises used: Subalgebra.add_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
hq :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R)) (AlgHom.range (esymmAlgHom (Fin m) R n))
    (HAdd.hAdd (α := ↥(symmetricSubalgebra (Fin m) R)) (β := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
        ↥(symmetricSubalgebra (Fin m) R)))

Tactic:
exact Subalgebra.add_mem _ hp hq

Premises used: Subalgebra.add_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
mul_X :
  Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R)) (AlgHom.range (esymmAlgHom (Fin m) R n))
    (HMul.hMul (α := ↥(symmetricSubalgebra (Fin m) R)) (β := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
        ↥(symmetricSubalgebra (Fin m) R)))
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (p * X i) :
      ↥(symmetricSubalgebra (Fin m) R))

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
mul_X :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R)) (AlgHom.range (esymmAlgHom (Fin m) R n))
    (HMul.hMul (α := ↥(symmetricSubalgebra (Fin m) R)) (β := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
        ↥(symmetricSubalgebra (Fin m) R)))

Tactic:
apply Subalgebra.mul_mem _ hp

Premises used: Subalgebra.mul_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ ∃ (x : MvPolynomial (Fin n) R),
    Eq (α := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) x :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
        ↥(symmetricSubalgebra (Fin m) R))

Tactic:
⟨X ⟨i, i.2.trans_le h⟩, ?_⟩

Premises used: MvPolynomial.X, Fin.isLt, Fin.mk, Fin.val, LT.lt.trans_le, Exists.intro
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
mul_X :
  Eq (α := ↥(symmetricSubalgebra (Fin m) R))
    ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) (X ⟨(↑i : ℕ), ⋯⟩) :
      ↥(symmetricSubalgebra (Fin m) R))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ ∃ (x : MvPolynomial (Fin n) R),
    Eq (α := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) x :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
        ↥(symmetricSubalgebra (Fin m) R))

Tactic:
refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
C :
  ∀ (r : R),
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R))
          ((MvPolynomial.C : (a : R) → MvPolynomial (Fin m) R) r) :
        ↥(symmetricSubalgebra (Fin m) R))
add :
  ∀ (p q : MvPolynomial (Fin m) R)
    (hp :
      Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
        (AlgHom.range (esymmAlgHom (Fin m) R n))
        ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
          ↥(symmetricSubalgebra (Fin m) R)))
    (hq :
      Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
        (AlgHom.range (esymmAlgHom (Fin m) R n))
        ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
          ↥(symmetricSubalgebra (Fin m) R))),
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (p + q) :
        ↥(symmetricSubalgebra (Fin m) R))
mul_X :
  ∀ (p : MvPolynomial (Fin m) R) (i : Fin m)
    (hp :
      Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
        (AlgHom.range (esymmAlgHom (Fin m) R n))
        ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
          ↥(symmetricSubalgebra (Fin m) R))),
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (p * X i) :
        ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
      ↥(symmetricSubalgebra (Fin m) R))

Tactic:
induction q using MvPolynomial.induction_on with
  | C r => rw [← algebraMap_eq, AlgHom.commutes]; apply Subalgebra.algebraMap_mem
  | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
  | mul_X p i hp =>
    rw [map_mul]
    apply Subalgebra.mul_mem _ hp
    rw [AlgHom.mem_range]
    refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩
    simp_rw [esymmAlgHom, aeval_X]

Premises used: MvPolynomial.aeval_X, map_add, AlgHom.mem_range, MvPolynomial.induction_on, MvPolynomial.esymmAlgHom, map_mul, MvPolynomial.algebraMap_eq, AlgHom.commutes, Subalgebra.algebraMap_mem, MvPolynomial.C
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ ≤ n
rw :
  Function.Surjective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra σ R))
    (Function.comp (β := ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R))
      (⇑(↑(renameSymmetricSubalgebra (Equiv.symm (Fintype.equivFin σ))) :
            ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R) →ₐ[R] ↥(symmetricSubalgebra σ R)) :
        (a : ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R)) → ↥(symmetricSubalgebra σ R))
      (⇑(esymmAlgHom (Fin (Fintype.card σ)) R n) :
        (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R)))
⊢ Function.Surjective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra σ R))
    (⇑(esymmAlgHom σ R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))

Tactic:
rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]

Premises used: MvPolynomial.rename_esymmAlgHom, Fintype.equivFin, AlgHom.coe_comp, Equiv.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra σ R))
    (Function.comp (β := ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R))
      (⇑(↑(renameSymmetricSubalgebra (Equiv.symm (Fintype.equivFin σ))) :
            ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R) →ₐ[R] ↥(symmetricSubalgebra σ R)) :
        (a : ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R)) → ↥(symmetricSubalgebra σ R))
      (⇑(esymmAlgHom (Fin (Fintype.card σ)) R n) :
        (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R)))

Tactic:
(AlgEquiv.surjective _).comp (esymmAlgHom_fin_surjective R hn)

Premises used: MvPolynomial.esymmAlgHom_fin_surjective, Function.Surjective.comp, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra σ R))
    (Function.comp (β := ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R))
      (⇑(↑(renameSymmetricSubalgebra (Equiv.symm (Fintype.equivFin σ))) :
            ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R) →ₐ[R] ↥(symmetricSubalgebra σ R)) :
        (a : ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R)) → ↥(symmetricSubalgebra σ R))
      (⇑(esymmAlgHom (Fin (Fintype.card σ)) R n) :
        (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R)))

Tactic:
exact (AlgEquiv.surjective _).comp (esymmAlgHom_fin_surjective R hn)

Premises used: MvPolynomial.esymmAlgHom_fin_surjective, Function.Surjective.comp, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ = n
i : Fin n
⊢ Function.Injective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra σ R))
    (⇑(esymmAlgHom σ R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))

Tactic:
esymmAlgHom_injective R hn.ge

Premises used: Eq.ge, MvPolynomial.esymmAlgHom_injective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ = n
i : Fin n
apply_fun :
  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))
⊢ Eq.{u_3 + 1} (α := MvPolynomial (Fin n) 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))
          ⋯) :
      MvPolynomial (Fin n) R)
    (X i : MvPolynomial (Fin n) R)

Tactic:
apply_fun esymmAlgHom σ R n using esymmAlgHom_injective R hn.ge

Premises used: Eq.ge, MvPolynomial.esymmAlgHom, MvPolynomial.esymmAlgHom_injective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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))
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)) ⋯)
    ((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)) ⋯ :
        (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))

Tactic:
simp_rw [esymmAlgEquiv, AlgEquiv.ofBijective_apply_symm_apply, esymmAlgHom, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.esymmAlgEquiv, MvPolynomial.esymmAlgHom, AlgEquiv.ofBijective_apply_symm_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
pos : ∀ (h1 : t.2 ∈ t.1), (t.1.erase t.2, t.2) ≠ t
neg : ∀ (h1 : t.2 ∉ t.1), (cons t.2 t.1 h1, 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

Tactic:
split_ifs with h1
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
pos : ∀ (ht : (t.1.erase t.2, t.2) = t), False
⊢ (t.1.erase t.2, t.2) ≠ t

Tactic:
by_contra ht
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
ht : (t.1.erase t.2, t.2) = t
⊢ (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1

Tactic:
rw [← ht] at h1
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
ht : (t.1.erase t.2, t.2) = t
h1₁ : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
⊢ (t.1.erase t.2, t.2) = t

Tactic:
rw [← ht] at h1
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
ht : (t.1.erase t.2, t.2) = t
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
neg : ∀ (ht : (cons t.2 t.1 h1, t.2) = t), False
⊢ (cons t.2 t.1 h1, t.2) ≠ t

Tactic:
by_contra ht
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
ht : (cons t.2 t.1 h1, t.2) = t
⊢ (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1

Tactic:
rw [← ht] at h1
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
ht : (cons t.2 t.1 h1, t.2) = t
h1₁ : (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) = t

Tactic:
rw [← ht] at h1
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h1_1 : t.2 ∉ t.1
h1 : (cons t.2 t.1 h1_1, t.2).2 ∉ (cons t.2 t.1 h1_1, t.2).1
ht : (cons t.2 t.1 h1_1, t.2) = t
⊢ False

Tactic:
simp_all
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h : t.2 ∈ t.1
⊢ pairMap σ t = (t.1.erase t.2, t.2)

Tactic:
simp [pairMap, h]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairMap
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
h : t.2 ∉ t.1
⊢ pairMap σ t = (cons t.2 t.1 h, t.2)

Tactic:
simp [pairMap, h]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairMap
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
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
⊢ pairMap σ (pairMap σ t) = t

Tactic:
rw [pairMap, pairMap]

Premises used: _private.0.MvPolynomial.NewtonIdentities.pairMap
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
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
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 ⋯, (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

Tactic:
split_ifs with h1 h2 h3
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
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:
simp at h2
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : DecidableEq σ
t : Finset σ × σ
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

Tactic:
simp [insert_erase h1]

Premises used: Finset.insert_erase
-- 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 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:
simp_all