awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
i : ℕ
him : i + 1 ≤ m
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
i : ℕ
him : i + 1 ≤ m
h : Nontrivial R
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R (i + 1))

Tactic:
(supDegree_monic_esymm him).2

Premises used: And.right, _private.0.MvPolynomial.supDegree_monic_esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
i : ℕ
him : i + 1 ≤ m
h : Nontrivial R
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R (i + 1))

Tactic:
exact (supDegree_monic_esymm him).2

Premises used: And.right, _private.0.MvPolynomial.supDegree_monic_esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
i : ℕ
him : i ≤ m
zero :
  ∀ (him : 0 ≤ m),
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R 0)
succ :
  ∀ (i : ℕ) (him : i + 1 ≤ m),
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymm (Fin m) R (i + 1))
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R i)

Tactic:
cases i with
  | zero =>
    rw [esymm_zero]
    exact monic_one toLex.injective
  | succ i =>
    nontriviality R
    exact (supDegree_monic_esymm him).2

Premises used: Fin.succ, AddMonoidAlgebra.monic_one, And.right, AddMonoidAlgebra.zero, _private.0.MvPolynomial.supDegree_monic_esymm, Equiv.injective, MvPolynomial.esymm_zero, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
zero :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      ((C : (a : R) → MvPolynomial (Fin m) R) r) =
    r
zero₁ zero₂ : r = r
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) (n := n) 0 r) =
    r

Tactic:
rw [esymmAlgHom_zero, leadingCoeff_toLex_C]

Premises used: MvPolynomial.leadingCoeff_toLex_C, MvPolynomial.esymmAlgHom_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) f r) =
    r
add_single : Function.Injective (α := Fin m →₀ ℕ) (β := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
add_single₁ :
  ∀ (a1 a2 : Fin m →₀ ℕ),
    (toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (a1 + a2) =
      HAdd.hAdd (α := Lex (Fin m →₀ ℕ)) (β := Lex (Fin m →₀ ℕ))
        ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) a1 : Lex (Fin m →₀ ℕ))
        ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) a2 : Lex (Fin m →₀ ℕ))
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r) =
    r

Tactic:
rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
        ih]

Premises used: AddMonoidAlgebra.Monic.pow, AddMonoidAlgebra.Monic.leadingCoeff_mul_eq_left, Fin.isLt, toLex_add, MvPolynomial.monic_esymm, MvPolynomial.esymmAlgHomMonomial_single_one, LT.lt.trans_le, MvPolynomial.esymmAlgHomMonomial_add, Equiv.injective, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) f r) =
    r
⊢ Function.Injective (α := Fin m →₀ ℕ) (β := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))

Tactic:
toLex.injective

Premises used: Equiv.injective, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) f r) =
    r
⊢ ∀ (a1 a2 : Fin m →₀ ℕ),
    (toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (a1 + a2) =
      HAdd.hAdd (α := Lex (Fin m →₀ ℕ)) (β := Lex (Fin m →₀ ℕ))
        ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) a1 : Lex (Fin m →₀ ℕ))
        ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) a2 : Lex (Fin m →₀ ℕ))

Tactic:
toLex_add

Premises used: toLex_add
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hnm : n ≤ m
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : b ≠ 0
ih :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) f r) =
    r
⊢ Function.Injective (α := Fin m →₀ ℕ) (β := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))

Tactic:
exacts [toLex.injective, toLex_add]

Premises used: toLex_add, Equiv.injective, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
t : Fin n →₀ ℕ
hnm : n ≤ m
zero :
  leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) (n := n) 0 r) =
    r
add_single :
  ∀ (i : Fin n) (b : ℕ) (f : Fin n →₀ ℕ),
    i ∉ f.support →
      b ≠ 0 →
        ∀
          (ih :
            leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
                (esymmAlgHomMonomial (Fin m) f r) =
              r),
          leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
              (esymmAlgHomMonomial (Fin m) (f + fun₀ | i => b) r) =
            r
⊢ leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymmAlgHomMonomial (Fin m) t r) =
    r

Tactic:
induction t using Finsupp.induction₂ with
  | zero => rw [esymmAlgHom_zero, leadingCoeff_toLex_C]
  | add_single i _ _ _ _ ih =>
    rw [esymmAlgHomMonomial_add, esymmAlgHomMonomial_single_one,
        ((monic_esymm <| i.2.trans_le hnm).pow toLex_add toLex.injective).leadingCoeff_mul_eq_left,
        ih]
    exacts [toLex.injective, toLex_add]

Premises used: toLex_add, MvPolynomial.leadingCoeff_toLex_C, MvPolynomial.esymmAlgHom_zero, MvPolynomial.esymmAlgHomMonomial_single_one, AddMonoidAlgebra.zero, MvPolynomial.esymmAlgHomMonomial_add, Equiv.injective, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
t : Fin n →₀ ℕ
hnm : n ≤ m
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
zero :
  Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((C : (a : R) → MvPolynomial (Fin m) R) r))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
zero₁ :
  Eq (α := (a : Fin m) → ℕ) (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ) 0) : (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
zero₂ :
  Eq (α := (a : Fin m) → ℕ) (⇑0 : (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑0 : (a : Fin n) → ℕ))
zero₃ : Eq (α := (a : Fin m) → ℕ) (0 : (a : Fin m) → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) 0 : Fin m → ℕ)
⊢ 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:
simp_rw [esymmAlgHom_zero, supDegree_toLex_C, ofLex_zero, Finsupp.coe_zero, map_zero]

Premises used: map_zero, MvPolynomial.supDegree_toLex_C, MvPolynomial.esymmAlgHom_zero, Finsupp.coe_zero, ofLex_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : 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) → ℕ))
⊢ (↑i : ℕ) < m

Tactic:
have := i.2.trans_le hnm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : 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) → ℕ))
this : (↑i : ℕ) < m
add_single :
  Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R ((↑i : ℕ) + 1))
add_single₁ :
  Monic (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (HPow.hPow (α := MvPolynomial (Fin m) R) (esymm (Fin m) R ((↑i : ℕ) + 1)) b)
add_single₂ : Ne (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
⊢ 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:
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]

Premises used: ofLex_add, Nat.cast_id, toLex_add, map_add, MvPolynomial.supDegree_esymm, Finsupp.coe_add, Finsupp.coe_smul, MvPolynomial.esymmAlgHomMonomial_single_one, AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left, AddMonoidAlgebra.Monic.supDegree_pow, MvPolynomial.esymmAlgHomMonomial_add, ofLex_smul, Equiv.injective, nsmul_one, map_nsmul, Finsupp.smul_single, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : 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) → ℕ))
this : (↑i : ℕ) < m
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R ((↑i : ℕ) + 1))

Tactic:
monic_esymm this

Premises used: MvPolynomial.monic_esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : 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) → ℕ))
this : (↑i : ℕ) < m
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (esymm (Fin m) R ((↑i : ℕ) + 1))

Tactic:
exact monic_esymm this

Premises used: MvPolynomial.monic_esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : 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) → ℕ))
this : (↑i : ℕ) < m
⊢ Monic (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (HPow.hPow (α := MvPolynomial (Fin m) R) (esymm (Fin m) R ((↑i : ℕ) + 1)) b)

Tactic:
(monic_esymm this).pow toLex_add toLex.injective

Premises used: AddMonoidAlgebra.Monic.pow, toLex_add, MvPolynomial.monic_esymm, Equiv.injective, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : 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) → ℕ))
this : (↑i : ℕ) < m
⊢ Monic (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
    (HPow.hPow (α := MvPolynomial (Fin m) R) (esymm (Fin m) R ((↑i : ℕ) + 1)) b)

Tactic:
exact (monic_esymm this).pow toLex_add toLex.injective

Premises used: AddMonoidAlgebra.Monic.pow, toLex_add, MvPolynomial.monic_esymm, Equiv.injective, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
r : R
hr : r ≠ 0
hnm : n ≤ m
inst_1 : Nontrivial R
i : Fin n
b : ℕ
f : Fin n →₀ ℕ
h : i ∉ f.support
h_1 : 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) → ℕ))
this : (↑i : ℕ) < m
add_single : ¬Eq (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0
add_single₁ :
  ¬leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (esymmAlgHomMonomial (Fin m) f r) =
      0
add_single₂ add_single₃ add_single₄ add_single₅ : ¬r = 0
⊢ Ne (α := R[Fin m →₀ ℕ]) (esymmAlgHomMonomial (Fin m) f r) 0

Tactic:
rwa [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_esymmAlgHomMonomial _ hnm]

Premises used: 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 : 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) → ℕ))
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) → ℕ))
⊢ 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) → ℕ))

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]

Premises used: ofLex_add, Nat.cast_id, MvPolynomial.leadingCoeff_esymmAlgHomMonomial, AddMonoidAlgebra.leadingCoeff_eq_zero, map_zero, toLex_add, map_add, Ne, MvPolynomial.supDegree_toLex_C, Finsupp.coe_add, Finsupp.coe_smul, MvPolynomial.esymmAlgHom_zero, MvPolynomial.esymmAlgHomMonomial_single_one, AddMonoidAlgebra.zero, AddMonoidAlgebra.Monic.supDegree_mul_of_ne_zero_left, AddMonoidAlgebra.Monic.supDegree_pow, MvPolynomial.esymmAlgHomMonomial_add, ofLex_smul, Equiv.injective, nsmul_one, map_nsmul, Finsupp.smul_single, Finsupp.coe_zero, ofLex_zero, toLex
-- 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
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 : σ) → ℕ)
inr :
  ∀ (h0 : p ≠ 0),
    Antitone (α := σ) (β := ℕ)
      (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
        (a : σ) → ℕ)
⊢ Antitone (α := σ) (β := ℕ)
    (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p) : σ →₀ ℕ) :
      (a : σ) → ℕ)

Tactic:
obtain rfl | h0 := eq_or_ne p 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder σ
hp : IsSymmetric.{u_1, u_3} (σ := σ) (R := R) 0
⊢ Antitone.{u_1, 0} (α := σ) (β := ℕ) (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) 0 : σ →₀ ℕ) : (a : σ) → ℕ)

Tactic:
Pi.zero_mono

Premises used: Antitone, Pi.zero_mono
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : LinearOrder σ
hp : IsSymmetric.{u_1, u_3} (σ := σ) (R := R) 0
⊢ Antitone.{u_1, 0} (α := σ) (β := ℕ) (⇑((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) 0 : σ →₀ ℕ) : (a : σ) → ℕ)

Tactic:
exact Pi.zero_mono

Premises used: Pi.zero_mono
-- 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
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
⊢ ∀ ⦃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 :
          ℕ)

Tactic:
by_contra! ⟨i, j, hle, hlt⟩
-- 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 (α := 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 : σ →₀ ℕ
apply₁ :
  Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
      ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) ∈
    p.support
⊢ False

Tactic:
apply (le_sup (s := p.support) (f := toLex) _).not_gt

Premises used: LE.le.not_gt, Finset.le_sup
-- 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 :
      ℕ)
rw : coeff ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) p ≠ 0
d : σ →₀ ℕ
⊢ Finsupp.mapDomain (α := σ) (⇑(Equiv.swap i j) : (a : σ) → σ)
      ((ofLex : (a : Lex (σ →₀ ℕ)) → σ →₀ ℕ) (supDegree (⇑toLex : (a : σ →₀ ℕ) → Lex (σ →₀ ℕ)) p)) ∈
    p.support

Tactic:
rw [← hp (Equiv.swap i j), mem_support_iff, coeff_rename_mapDomain _ (Equiv.injective _)]

Premises used: MvPolynomial.mem_support_iff, Equiv.swap, MvPolynomial.coeff_rename_mapDomain, Equiv.injective