awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
t : Fin n →₀ ℕ
hnm : n ≤ m
inst_1 : Nontrivial R
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) t r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ))
have zero : Eq (α := (a : Fin m) → ℕ)
  (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (esymmAlgHomMonomial (Fin m) (n := n) 0 r))) :
    (a : Fin m) → ℕ)
  ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
Tactic: induction t using Finsupp.induction₂ with
  | zero => simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]
  | add_single i _ _ _ _ ih =>
    have := i.2.trans_le hnm
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add, ofLex_add, Finsupp.coe_add,
        ih, Finsupp.coe_add, map_add, Monic.supDegree_pow rfl toLex_add toLex.injective, ofLex_smul,
        Finsupp.coe_smul, supDegree_esymm this, ← map_nsmul, ← Finsupp.coe_smul,
        Finsupp.smul_single, nsmul_one, Nat.cast_id]
    · exact monic_esymm this
    · exact (monic_esymm this).pow toLex_add toLex.injective
    · rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
t : Fin n →₀ ℕ
hnm : n ≤ m
inst_1 : Nontrivial R
zero :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) (n := n) 0 r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymmAlgHomMonomial (Fin m) t r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑t : (a : Fin n) → ℕ))
have add_single : ∀ (i : Fin n) (b : ℕ) (f : Fin n →₀ ℕ),
  i ∉ f.support →
    b ≠ 0 →
      ∀
        (ih :
          Eq (α := (a : Fin m) → ℕ)
            (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
                  (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
                    (esymmAlgHomMonomial (Fin m) f r))) :
              (a : Fin m) → ℕ)
            ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑f : (a : Fin n) → ℕ))),
        Eq (α := (a : Fin m) → ℕ)
          (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
                (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
                  (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r))) :
            (a : Fin m) → ℕ)
          ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑(f + fun₀ | i => b) : (a : Fin n) → ℕ))
Tactic: induction t using Finsupp.induction₂ with
  | zero => simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]
  | add_single i _ _ _ _ ih =>
    have := i.2.trans_le hnm
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        Monic.supDegree_mul_of_ne_zero_left toLex.injective toLex_add, ofLex_add, Finsupp.coe_add,
        ih, Finsupp.coe_add, map_add, Monic.supDegree_pow rfl toLex_add toLex.injective, ofLex_smul,
        Finsupp.coe_smul, supDegree_esymm this, ← map_nsmul, ← Finsupp.coe_smul,
        Finsupp.smul_single, nsmul_one, Nat.cast_id]
    · exact monic_esymm this
    · exact (monic_esymm this).pow toLex_add toLex.injective
    · rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]
Cleared hypotheses: t
-- 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
⊢ Antitone (α := σ) (β := ℕ)
    (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
      (a : σ) → ℕ)
have inl : ∀ (hp : IsSymmetric.{u_1, u_3} (σ := σ) (R := R) 0),
  Antitone.{u_1, 0} (α := σ) (β := ℕ)
    (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ)
            (supDegree.{u_3, u_1, u_1} (R := R) (A := σ →₀ ℕ) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) 0) :
          σ →₀ ℕ) :
      (a : σ) → ℕ)
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:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
inl :
  ∀ (hp : IsSymmetric.{u_1, u_3} (σ := σ) (R := R) 0),
    Antitone.{u_1, 0} (α := σ) (β := ℕ)
      (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ)
              (supDegree.{u_3, u_1, u_1} (R := R) (A := σ →₀ ℕ) (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) 0) :
            σ →₀ ℕ) :
        (a : σ) → ℕ)
⊢ Antitone (α := σ) (β := ℕ)
    (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
      (a : σ) → ℕ)
have inr : ∀ (h0 : p ≠ 0),
  Antitone (α := σ) (β := ℕ)
    (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
      (a : σ) → ℕ)
Tactic: obtain rfl | h0 := eq_or_ne p 0
-- 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
⊢ ∀ ⦃a b : σ⦄,
    a ≤ b →
      LE.le (α := ℕ)
        ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
              (a : σ) → ℕ)
            b :
          ℕ)
        ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
              (a : σ) → ℕ)
            a :
          ℕ)
have inr : ∀ (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 :
        ℕ)),
  False
Tactic: by_contra! ⟨i, j, hle, hlt⟩
-- 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 :
      ℕ)
⊢ False
have inr : LT.lt (α := Lex (σ →₀ ℕ)) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) : Lex (σ →₀ ℕ))
  ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
      (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
        ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
    Lex (σ →₀ ℕ))
Tactic: apply (le_sup (s := p.support) (f := toLex) _).not_gt
-- 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 :
  LT.lt (α := Lex (σ →₀ ℕ)) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) : Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
      Lex (σ →₀ ℕ))
⊢ False
have apply : σ →₀ ℕ
Tactic: apply (le_sup (s := p.support) (f := toLex) _).not_gt
-- 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 :
  LT.lt (α := Lex (σ →₀ ℕ)) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) : Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
      Lex (σ →₀ ℕ))
apply : σ →₀ ℕ
⊢ False
have apply₁ : Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
    ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) ∈
  p.support
Tactic: apply (le_sup (s := p.support) (f := toLex) _).not_gt
-- 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 :
      ℕ)
⊢ Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
      ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) ∈
    p.support
have rw : coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p ≠ 0
Tactic: rw [← hp (Equiv.swap i j), mem_support_iff, coeff_rename_mapDomain _ (Equiv.injective _)]
-- 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 :
      ℕ)
rw : coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p ≠ 0
⊢ Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
      ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) ∈
    p.support
have d : σ →₀ ℕ
Tactic: rw [← hp (Equiv.swap i j), mem_support_iff, coeff_rename_mapDomain _ (Equiv.injective _)]
-- 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 :
      ℕ)
⊢ LT.lt (α := Lex (σ →₀ ℕ)) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) : Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
      Lex (σ →₀ ℕ))
have inr : ∀ (k : σ) (hk : (fun (x1 x2 : σ) ↦ x1 < x2) k i),
  Eq (α := (@fun {i : σ} ↦ ℕ) k)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ)
              ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
                  (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
                    ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
                Lex (σ →₀ ℕ)) :
            σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)
Tactic: refine ⟨i, fun k hk ↦ ?_, ?_⟩
-- 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 :
  ∀ (k : σ) (hk : (fun (x1 x2 : σ) ↦ x1 < x2) k i),
    Eq (α := (@fun {i : σ} ↦ ℕ) k)
      ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
            (a : σ) → ℕ)
          k :
        ℕ)
      ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ)
                ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
                    (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
                      ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
                  Lex (σ →₀ ℕ)) :
              σ →₀ ℕ) :
            (a : σ) → ℕ)
          k :
        ℕ)
⊢ LT.lt (α := Lex (σ →₀ ℕ)) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) : Lex (σ →₀ ℕ))
    ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
        (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
      Lex (σ →₀ ℕ))
have inr₁ : (@fun {i : σ} (x1 x2 : ℕ) ↦ x1 < x2) i
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
      (a : σ) → ℕ)
    i)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ)
          ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
              (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
                ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
            Lex (σ →₀ ℕ)) :
        σ →₀ ℕ) :
      (a : σ) → ℕ)
    i)
Tactic: refine ⟨i, fun k hk ↦ ?_, ?_⟩
-- 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 :
      ℕ)
k : σ
hk : (fun (x1 x2 : σ) ↦ x1 < x2) k i
⊢ Eq (α := (@fun {i : σ} ↦ ℕ) k)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ)
              ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
                  (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
                    ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
                Lex (σ →₀ ℕ)) :
            σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)
have inr : Eq (α := ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
        (a : σ) → ℕ)
      k :
    ℕ)
  ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
        (a : σ) → ℕ)
      k :
    ℕ)
Tactic: dsimp only [Pi.toLex_apply, ofLex_toLex]
-- 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 :
      ℕ)
⊢ (@fun {i : σ} (x1 x2 : ℕ) ↦ x1 < x2) i
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
        (a : σ) → ℕ)
      i)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ)
            ((toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))
                (Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
                  ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p))) :
              Lex (σ →₀ ℕ)) :
          σ →₀ ℕ) :
        (a : σ) → ℕ)
      i)
have inr : LT.lt (α := ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
        (a : σ) → ℕ)
      i :
    ℕ)
  ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
        (a : σ) → ℕ)
      i :
    ℕ)
Tactic: dsimp only [Pi.toLex_apply, ofLex_toLex]
-- 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 :
      ℕ)
k : σ
hk : (fun (x1 x2 : σ) ↦ x1 < x2) k i
| ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
        (a : σ) → ℕ)
      k :
    ℕ)
have rw : ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
        ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
      (a : σ) → ℕ)
    ((Equiv.swap i j : (a : σ) → σ) k : σ) :
  ℕ)
Tactic: rw [← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne]
-- 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 :
      ℕ)
k : σ
hk : (fun (x1 x2 : σ) ↦ x1 < x2) k i
⊢ Eq (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)
    ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
            ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
          (a : σ) → ℕ)
        k :
      ℕ)
have inr : Eq (α := ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
        (a : σ) → ℕ)
      k :
    ℕ)
  ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
        (a : σ) → ℕ)
      ((Equiv.swap i j : (a : σ) → σ) k : σ) :
    ℕ)
Tactic: conv_rhs => rw [← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne]
-- 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 :
      ℕ)
k : σ
hk : (fun (x1 x2 : σ) ↦ x1 < x2) k i
⊢ Eq (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)
    ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
            ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
          (a : σ) → ℕ)
        ((Equiv.swap i j : (a : σ) → σ) k : σ) :
      ℕ)
have inr : Eq (α := ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
        (a : σ) → ℕ)
      k :
    ℕ)
  ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
        (a : σ) → ℕ)
      k :
    ℕ)
Tactic: rw [Finsupp.mapDomain_apply (Equiv.injective _), supDegree]
-- 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 :
      ℕ)
⊢ LT.lt (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        i :
      ℕ)
    ((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 :
    ℕ)
  ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
        (a : σ) → ℕ)
      i :
    ℕ)
Tactic: apply hlt.trans_eq