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
inst : CommSemiring R
inst_1 : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt :
  LT.lt (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        i :
      ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        j :
      ℕ)
⊢ Eq (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        j :
      ℕ)
    ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
            ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
          (a : σ) → ℕ)
        i :
      ℕ)
have inr : Eq (α := ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) : (a : σ) → ℕ)
      j :
    ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) : (a : σ) → ℕ)
      ((Equiv.symm (Equiv.swap i j) : (a : σ) → σ) i : σ) :
    ℕ)
Tactic: simp_rw [Finsupp.mapDomain_equiv_apply, Equiv.symm_swap, Equiv.swap_apply_left]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt :
  LT.lt (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        i :
      ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        j :
      ℕ)
inr :
  Eq (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        j :
      ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        ((Equiv.symm (Equiv.swap i j) : (a : σ) → σ) i : σ) :
      ℕ)
⊢ Eq (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        j :
      ℕ)
    ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
            ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
          (a : σ) → ℕ)
        i :
      ℕ)
have inr₁ : Eq (α := ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) : (a : σ) → ℕ)
      j :
    ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) : (a : σ) → ℕ)
      ((Equiv.swap i j : (a : σ) → σ) i : σ) :
    ℕ)
Tactic: simp_rw [Finsupp.mapDomain_equiv_apply, Equiv.symm_swap, Equiv.swap_apply_left]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
⊢ Function.Injective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra (Fin m) R))
    (⇑(esymmAlgHom (Fin m) R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
have rw : ∀ (a : MvPolynomial (Fin n) R),
  Eq (α := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) a :
        ↥(symmetricSubalgebra (Fin m) R))
      (0 : ↥(symmetricSubalgebra (Fin m) R)) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
⊢ ∀ (a : MvPolynomial (Fin n) R),
    Eq (α := ↥(symmetricSubalgebra (Fin m) R))
        ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) a :
          ↥(symmetricSubalgebra (Fin m) R))
        (0 : ↥(symmetricSubalgebra (Fin m) R)) →
      a = 0
have refine : ∀ (p : MvPolynomial (Fin n) R) (hp : ¬p = 0),
  ¬Eq (α := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R))
      (0 : ↥(symmetricSubalgebra (Fin m) R))
Tactic: refine fun p ↦ (fun hp ↦ ?_).mtr
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
⊢ ¬Eq (α := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R))
      (0 : ↥(symmetricSubalgebra (Fin m) R))
have rw : ¬Eq.{u_3 + 1} (α := MvPolynomial (Fin m) R)
    (∑ i ∈ p.support,
      (↑((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))
    0
Tactic: rw [p.as_sum, map_sum (esymmAlgHom (Fin m) R n), ← Subalgebra.coe_eq_zero,
    AddSubmonoidClass.coe_finsetSum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
⊢ ¬Eq.{u_3 + 1} (α := MvPolynomial (Fin m) R)
      (∑ i ∈ p.support,
        (↑((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))
      0
have refine_1 : ∀ (t : Fin n →₀ ℕ) (ht : t ∈ p.support),
  Ne.{max (u_3 + 1) 1} (α := R[Fin m →₀ ℕ])
    (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
          ((monomial t : (a : R) → MvPolynomial (Fin n) R) (coeff t p))) :
      MvPolynomial (Fin m) R)
    0
Tactic: refine sum_ne_zero_of_injOn_supDegree (D := toLex) (support_nonempty.2 hp) (fun t ht ↦ ?_)
    (fun t ht s hs he ↦ DFunLike.ext' <| accumulate_injective h ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
refine_1 :
  ∀ (t : Fin n →₀ ℕ) (ht : t ∈ p.support),
    Ne.{max (u_3 + 1) 1} (α := R[Fin m →₀ ℕ])
      (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R) (coeff t p))) :
        MvPolynomial (Fin m) R)
      0
⊢ ¬Eq.{u_3 + 1} (α := MvPolynomial (Fin m) R)
      (∑ i ∈ p.support,
        (↑((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))
      0
have refine_2 : ∀ (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)),
  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: refine sum_ne_zero_of_injOn_supDegree (D := toLex) (support_nonempty.2 hp) (fun t ht ↦ ?_)
    (fun t ht s hs he ↦ DFunLike.ext' <| accumulate_injective h ?_)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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
⊢ Ne.{max (u_3 + 1) 1} (α := R[Fin m →₀ ℕ])
    (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
          ((monomial t : (a : R) → MvPolynomial (Fin n) R) (coeff t p))) :
      MvPolynomial (Fin m) R)
    0
have refine_1 : ¬coeff t p = 0
Tactic: rw [← esymmAlgHomMonomial, Ne, ← leadingCoeff_eq_zero toLex.injective,
      leadingCoeff_esymmAlgHomMonomial t h]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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
⊢ ¬coeff t p = 0
have refine_1 : ∀ (ht : coeff t p ≠ 0), ¬coeff t p = 0
Tactic: rwa [mem_support_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ 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 → ℕ)
have 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 → ℕ)
Tactic: rw [mem_coe, mem_support_iff] at ht hs
Cleared hypotheses: ht, s, hs, he
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  Eq (α := Lex (Fin m →₀ ℕ))
    (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R) (coeff t p))) :
        MvPolynomial (Fin m) R))
    (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
            ((monomial s : (a : R) → MvPolynomial (Fin n) R) (coeff s p))) :
        MvPolynomial (Fin m) R))
⊢ 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 → ℕ)
have refine_2 : ∀
  (he :
    Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (esymmAlgHomMonomial (Fin m) t (coeff t p)))
      (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
              ((monomial s : (a : R) → MvPolynomial (Fin n) R) (coeff s p))) :
          MvPolynomial (Fin m) R))),
  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: rwa [← esymmAlgHomMonomial, ← esymmAlgHomMonomial, ← ofLex_inj, DFunLike.ext'_iff,
       supDegree_esymmAlgHomMonomial ht t h, supDegree_esymmAlgHomMonomial hs s h] at he
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  Eq (α := Lex (Fin m →₀ ℕ))
    (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R) (coeff t p))) :
        MvPolynomial (Fin m) R))
    (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
            ((monomial s : (a : R) → MvPolynomial (Fin n) R) (coeff s p))) :
        MvPolynomial (Fin m) R))
refine_2 :
  ∀
    (he :
      Eq (α := Lex (Fin m →₀ ℕ))
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (esymmAlgHomMonomial (Fin m) t (coeff t p)))
        (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (↑((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))
                ((monomial s : (a : R) → MvPolynomial (Fin n) R) (coeff s p))) :
            MvPolynomial (Fin m) R))),
    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 → ℕ)
have refine_2₁ : ∀
  (he :
    Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (esymmAlgHomMonomial (Fin m) t (coeff t p)))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (esymmAlgHomMonomial (Fin m) s (coeff s p)))),
  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: rwa [← esymmAlgHomMonomial, ← esymmAlgHomMonomial, ← ofLex_inj, DFunLike.ext'_iff,
       supDegree_esymmAlgHomMonomial ht t h, supDegree_esymmAlgHomMonomial hs s h] at he
Cleared hypotheses: he
-- 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 : n ≤ Fintype.card σ
⊢ Function.Injective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra σ R))
    (⇑(esymmAlgHom σ R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
have 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)))
Tactic: rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
⊢ Function.Bijective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra (Fin n) R))
    (⇑(esymmAlgHom (Fin n) R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin n) R))
have 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))
Tactic: use esymmAlgHom_fin_injective R 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
⊢ 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 : ∀ (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: obtain rfl | h0 := eq_or_ne p 0
Cleared hypotheses: p, hp
-- 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
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)
⊢ 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₁ : ∀ (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)
Tactic: obtain rfl | h0 := eq_or_ne p 0
-- 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
⊢ 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 : ∀ (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)
Tactic: induction he : p.supDegree toLex using WellFoundedLT.induction generalizing p with | _ t ih
Cleared hypotheses: p, hp, h0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
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
⊢ 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 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)
Tactic: subst he
Cleared hypotheses: t, ih, he