awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0_1 : p ≠ 0
h0 : ¬coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) 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 :
      ℕ)
⊢ coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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 (σ →₀ ℕ))

Tactic:
⟨i, fun k hk ↦ ?_, ?_⟩

Premises used: Pi.Lex, And.intro, Exists.intro, Finsupp.Lex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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 :
        ℕ)
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)
⊢ 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:
refine ⟨i, fun k hk ↦ ?_, ?_⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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
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 :
      ℕ)
⊢ 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:
dsimp only [Pi.toLex_apply, ofLex_toLex]

Premises used: ofLex_toLex, Pi.toLex_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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 (α := ℕ)
    ((((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 :
      ℕ)
⊢ (@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:
dsimp only [Pi.toLex_apply, ofLex_toLex]

Premises used: ofLex_toLex, Pi.toLex_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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
rw :
  ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
        (a : σ) → ℕ)
      ((Equiv.swap i j : (a : σ) → σ) k : σ) :
    ℕ)
| ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
          ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
        (a : σ) → ℕ)
      k :
    ℕ)

Tactic:
rw [← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne]

Premises used: Equiv.swap_apply_of_ne_of_ne, LT.lt.trans_le, LT.lt.ne
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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
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 : σ) :
      ℕ)
⊢ 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:
conv_rhs => rw [← Equiv.swap_apply_of_ne_of_ne hk.ne (hk.trans_le hle).ne]

Premises used: Equiv.swap_apply_of_ne_of_ne, LT.lt.trans_le, LT.lt.ne
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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
inr :
  Eq (α := ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)
⊢ 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:
rw [Finsupp.mapDomain_apply (Equiv.injective _), supDegree]

Premises used: Finsupp.mapDomain_apply, AddMonoidAlgebra.supDegree, Equiv.injective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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 :
      ℕ)
    ((((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (p.support.sup (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ))) : σ →₀ ℕ) :
          (a : σ) → ℕ)
        k :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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 :
      ℕ)
    ((Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
            ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) :
          (a : σ) → ℕ)
        i :
      ℕ)
⊢ 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:
apply hlt.trans_eq

Premises used: LT.lt.trans_eq
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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 : σ) :
      ℕ)
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 : σ) :
      ℕ)
⊢ 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:
simp_rw [Finsupp.mapDomain_equiv_apply, Equiv.symm_swap, Equiv.swap_apply_left]

Premises used: Equiv.symm_swap, Finsupp.mapDomain_equiv_apply, Equiv.swap_apply_left
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
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
⊢ Function.Injective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra (Fin m) R))
    (⇑(esymmAlgHom (Fin m) R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R))

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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

Tactic:
fun p ↦ (fun hp ↦ ?_).mtr

Premises used: Function.mtr
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : n ≤ m
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))
⊢ ∀ (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:
refine fun p ↦ (fun hp ↦ ?_).mtr

Premises used: Function.mtr
-- 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
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
⊢ ¬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:
rw [p.as_sum, map_sum (esymmAlgHom (Fin m) R n), ← Subalgebra.coe_eq_zero,
    AddSubmonoidClass.coe_finsetSum]

Premises used: AddSubmonoidClass.coe_finsetSum, MvPolynomial.as_sum, map_sum, MvPolynomial.esymmAlgHom, Subalgebra.coe_eq_zero, Fin
-- 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
⊢ ¬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:
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 ?_)

Premises used: Iff.mpr, MvPolynomial.support_nonempty, DFunLike.ext', AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree, Fin.accumulate_injective
-- 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
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
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 → ℕ)
⊢ ¬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:
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 ?_)

Premises used: Iff.mpr, MvPolynomial.support_nonempty, DFunLike.ext', AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree, Fin.accumulate_injective
-- 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
refine_1 : ¬coeff t p = 0
⊢ 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:
rw [← esymmAlgHomMonomial, Ne, ← leadingCoeff_eq_zero toLex.injective,
      leadingCoeff_esymmAlgHomMonomial t h]

Premises used: MvPolynomial.esymmAlgHomMonomial, MvPolynomial.leadingCoeff_esymmAlgHomMonomial, AddMonoidAlgebra.leadingCoeff_eq_zero, Ne, Equiv.injective, toLex
-- 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
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (ht : coeff t p ≠ 0), ¬coeff t p = 0
⊢ ¬coeff t p = 0

Tactic:
rwa [mem_support_iff] at ht

Premises used: MvPolynomial.mem_support_iff