-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma IsSymmetric.antitone_supDegree [LinearOrder σ] {p : MvPolynomial σ R} (hp : p.IsSymmetric) :
    Antitone ↑(ofLex <| p.supDegree toLex)

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ ?m.79756 ∈ p.support

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

Result:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff ?d p ≠ 0

case d
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
⊢ Antitone ⇑(ofLex (supDegree (⇑toLex) p))

Tactic:
obtain rfl | h0 := eq_or_ne p 0

Result:
case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
hp : IsSymmetric 0
⊢ Antitone ⇑(ofLex (supDegree (⇑toLex) 0))

case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
⊢ Antitone ⇑(ofLex (supDegree (⇑toLex) p))

Proof state:
case inr.intro.intro.intro
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ p.support.sup ⇑toLex < toLex ?m.79756

σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ

σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ ?m.79756 ∈ p.support

Tactic:
pick_goal 3

Result:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ ?m.79756 ∈ p.support

case inr.intro.intro.intro
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ p.support.sup ⇑toLex < toLex ?m.79756

σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ

Proof state:
case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
hp : IsSymmetric 0
⊢ Antitone ⇑(ofLex (supDegree (⇑toLex) 0))

Tactic:
rw [supDegree_zero, Finsupp.bot_eq_zero]

Result:
case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
hp : IsSymmetric 0
⊢ Antitone ⇑(ofLex 0)

Proof state:
case inr.intro.intro.intro.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (fun {i} x1 x2 => x1 < x2) ((ofLex (p.support.sup ⇑toLex)) i)
    ((ofLex (toLex (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))))) i)

Tactic:
dsimp only [Pi.toLex_apply, ofLex_toLex]

Result:
case inr.intro.intro.intro.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (ofLex (p.support.sup ⇑toLex)) i < (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) i

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff ?d p ≠ 0

case d
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ

Tactic:
rw [Ne, ← leadingCoeff_eq_zero toLex.injective, leadingCoeff_toLex] at h0

Result:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0✝ : p ≠ 0
h0 : ¬coeff (ofLex (supDegree (⇑toLex) p)) p = 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ coeff (?m.80270 i j hle hlt) p ≠ 0

Proof state:
case inr.intro.intro.intro
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ False

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

Result:
case inr.intro.intro.intro
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ p.support.sup ⇑toLex < toLex ?m.79756

σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ σ →₀ ℕ

σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ ?m.79756 ∈ p.support

Proof state:
case inr.intro.intro.intro.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (ofLex (p.support.sup ⇑toLex)) i < (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) i

Tactic:
apply hlt.trans_eq

Result:
case inr.intro.intro.intro.refine_2
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
⊢ (ofLex (supDegree (⇑toLex) p)) j = (Finsupp.mapDomain (⇑(Equiv.swap i j)) (ofLex (supDegree (⇑toLex) p))) i