awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
have 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) → ℕ)
Tactic: rw [← ofLex_inj, DFunLike.ext'_iff, supDegree_esymmAlgHomMonomial _ _ le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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) → ℕ)
⊢ 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)
have rw₁ : leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p ≠ 0
Tactic: rw [← ofLex_inj, DFunLike.ext'_iff, supDegree_esymmAlgHomMonomial _ _ le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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) → ℕ))
⊢ leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p ≠ 0
have rwa : ¬leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = 0
Tactic: rwa [Ne, leadingCoeff_eq_zero toLex.injective]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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
⊢ leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p ≠ 0
have rwa₁ : ¬p = 0
Tactic: rwa [Ne, leadingCoeff_eq_zero toLex.injective]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
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) → ℕ))
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ 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)
have 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)
Tactic: obtain he | hne := eq_or_ne p (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ 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)
have 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)
Tactic: obtain he | hne := eq_or_ne p (esymmAlgHomMonomial _ t <| p.leadingCoeff toLex)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
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)
have right : ∀
  (this :
    LT.lt (α := Lex (Fin n →₀ ℕ))
      (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
        (p -
          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)),
  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: have := (supDegree_sub_lt_of_leadingCoeff_eq toLex.injective hd.symm ?_).resolve_right hne
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
hne :
  p ≠
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
right :
  ∀
    (this :
      LT.lt (α := Lex (Fin n →₀ ℕ))
        (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
          (p -
            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)),
    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)
have right₁ : leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p =
  leadingCoeff (A := Fin n →₀ ℕ) (B := Lex (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) :
      MvPolynomial (Fin n) R)
Tactic: have := (supDegree_sub_lt_of_leadingCoeff_eq toLex.injective hd.symm ?_).resolve_right hne
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
hne :
  p ≠
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
this :
  LT.lt (α := Lex (Fin n →₀ ℕ))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (p -
        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)
⊢ 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)
have right : p -
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p) ≠
  0
Tactic: specialize ih _ this _ (Subalgebra.sub_mem _ hp <| isSymmetric_esymmAlgHomMonomial _ _) _ rfl