awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ (↑p.support : Set (Fin n →₀ ℕ))
s : Fin n →₀ ℕ
hs : s ∈ (↑p.support : Set (Fin n →₀ ℕ))
he :
  Eq (α := Lex (Fin m →₀ ℕ))
    (Function.comp.{1, max 1 (u_3 + 1), 1} (β := R[Fin m →₀ ℕ])
      (supDegree (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)))
      (fun (i : Fin n →₀ ℕ) ↦
        (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
              ((monomial i : (a : R) → MvPolynomial (Fin n) R) (coeff i p))) :
          MvPolynomial (Fin m) R))
      t)
    (Function.comp.{1, max 1 (u_3 + 1), 1} (β := R[Fin m →₀ ℕ])
      (supDegree (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)))
      (fun (i : Fin n →₀ ℕ) ↦
        (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
              ((monomial i : (a : R) → MvPolynomial (Fin n) R) (coeff i p))) :
          MvPolynomial (Fin m) R))
      s)
refine_2 :
  ∀ (ht : coeff t p ≠ 0) (s : Fin n →₀ ℕ) (hs : coeff s p ≠ 0)
    (he :
      Eq (α := Lex (Fin m →₀ ℕ))
        (Function.comp.{1, max 1 (u_3 + 1), 1} (β := R[Fin m →₀ ℕ])
          (supDegree (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)))
          (fun (i : Fin n →₀ ℕ) ↦
            (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
                  ((monomial i : (a : R) → MvPolynomial (Fin n) R) (coeff i p))) :
              MvPolynomial (Fin m) R))
          t)
        (Function.comp.{1, max 1 (u_3 + 1), 1} (β := R[Fin m →₀ ℕ])
          (supDegree (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)))
          (fun (i : Fin n →₀ ℕ) ↦
            (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
                  ((monomial i : (a : R) → MvPolynomial (Fin n) R) (coeff i p))) :
              MvPolynomial (Fin m) R))
          s)),
    Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)
⊢ Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑s : (a : Fin n) → ℕ) : Fin m → ℕ)

Tactic:
rw [mem_coe, mem_support_iff] at ht hs

Premises used: MvPolynomial.mem_support_iff, Finset.mem_coe
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : n ≤ Fintype.card σ
rw :
  Function.Injective (α := 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.Injective (α := 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 : n ≤ Fintype.card σ
⊢ Function.Injective (α := 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.injective _).comp (esymmAlgHom_fin_injective R hn)

Premises used: Function.Injective.comp, MvPolynomial.esymmAlgHom_fin_injective, AlgEquiv.injective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : n ≤ Fintype.card σ
⊢ Function.Injective (α := 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.injective _).comp (esymmAlgHom_fin_injective R hn)

Premises used: Function.Injective.comp, MvPolynomial.esymmAlgHom_fin_injective, AlgEquiv.injective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
right :
  Function.Surjective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra (Fin n) R))
    (⇑(esymmAlgHom (Fin n) R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin n) R))
⊢ Function.Bijective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra (Fin n) R))
    (⇑(esymmAlgHom (Fin n) R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin n) R))

Tactic:
use esymmAlgHom_fin_injective R le_rfl

Premises used: le_rfl, MvPolynomial.esymmAlgHom_fin_injective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
right :
  ∀ (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) 0),
    Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
      (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
        Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) 0 hp)
right₁ :
  ∀ (h0 : p ≠ 0),
    Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
      (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
        Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)

Tactic:
obtain rfl | h0 := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) 0
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) 0 hp)

Tactic:
Subalgebra.zero_mem _

Premises used: Set.Mem, Subalgebra.zero_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) 0
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) 0 hp)

Tactic:
exact Subalgebra.zero_mem _

Premises used: Subalgebra.zero_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
right :
  ∀ (t : Lex (Fin n →₀ ℕ))
    (ih :
      ∀ y < t,
        ∀ (p : MvPolynomial (Fin n) R)
          (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p)
          (h0 : p ≠ 0) (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
          Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
            (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
              Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp))
    (p : MvPolynomial (Fin n) R)
    (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
    (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = t),
    Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
      (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
        Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)

Tactic:
induction he : p.supDegree toLex using WellFoundedLT.induction generalizing p with | _ t ih

Premises used: WellFoundedLT.induction, AddMonoidAlgebra.supDegree, DFunLike.coe, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
t : Lex (Fin n →₀ ℕ)
ih :
  ∀ y < t,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = t
⊢ ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)

Tactic:
subst he
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
rw :
  Eq (α := (a : Fin n) → ℕ) ((accumulate n n : (a : Fin n → ℕ) → Fin n → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin n → ℕ)
    ((⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ) :
      (a : Fin n) → ℕ)
rw₁ : leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p ≠ 0
⊢ Eq (α := Lex (Fin n →₀ ℕ))
    (supDegree (A := Fin n →₀ ℕ) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)

Tactic:
rw [← ofLex_inj, DFunLike.ext'_iff, supDegree_esymmAlgHomMonomial _ _ le_rfl]

Premises used: le_rfl, MvPolynomial.supDegree_esymmAlgHomMonomial, DFunLike.ext'_iff, ofLex_inj
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
⊢ Eq (α := (a : Fin n) → ℕ) ((accumulate n n : (a : Fin n → ℕ) → Fin n → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin n → ℕ)
    ((⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ) :
      (a : Fin n) → ℕ)

Tactic:
accumulate_invAccumulate le_rfl hp.antitone_supDegree

Premises used: le_rfl, Fin.invAccumulate, Fin.accumulate_invAccumulate, MvPolynomial.IsSymmetric.antitone_supDegree
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
⊢ Eq (α := (a : Fin n) → ℕ) ((accumulate n n : (a : Fin n → ℕ) → Fin n → ℕ) (⇑t : (a : Fin n) → ℕ) : Fin n → ℕ)
    ((⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ) :
      (a : Fin n) → ℕ)

Tactic:
exact accumulate_invAccumulate le_rfl hp.antitone_supDegree

Premises used: le_rfl, Fin.accumulate_invAccumulate, MvPolynomial.IsSymmetric.antitone_supDegree
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
rwa : ¬leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ¬p = 0
⊢ leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p ≠ 0

Tactic:
rwa [Ne, leadingCoeff_eq_zero toLex.injective]

Premises used: AddMonoidAlgebra.leadingCoeff_eq_zero, Ne, Equiv.injective, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
⊢ Eq (α := Lex (Fin n →₀ ℕ))
    (supDegree (A := Fin n →₀ ℕ) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)

Tactic:
have hd :
      (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex).supDegree toLex = p.supDegree toLex := by
    rw [← ofLex_inj, DFunLike.ext'_iff, supDegree_esymmAlgHomMonomial _ _ le_rfl]
    · exact accumulate_invAccumulate le_rfl hp.antitone_supDegree
    · rwa [Ne, leadingCoeff_eq_zero toLex.injective]
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
hd :
  Eq (α := Lex (Fin n →₀ ℕ))
    (supDegree (A := Fin n →₀ ℕ) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
right :
  ∀
    (he :
      p =
        esymmAlgHomMonomial (Fin n) t
          (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)),
    Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
      (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
        Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
right₁ :
  ∀
    (hne :
      p ≠
        esymmAlgHomMonomial (Fin n) t
          (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)),
    Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
      (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
        Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)

Tactic:
obtain he | hne := eq_or_ne p (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex)

Premises used: MvPolynomial.esymmAlgHomMonomial, eq_or_ne, AddMonoidAlgebra.leadingCoeff, DFunLike.coe, toLex