-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
private lemma supDegree_monic_esymm [Nontrivial R] {i : ℕ} (him : i < m) :
    supDegree toLex (esymm (Fin m) R (i + 1)) =
      toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun _ _ ↦ 1) ∧
    Monic toLex (esymm (Fin m) R (i + 1))

Proof state:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ supDegree (⇑toLex) ((fun s => (monomial (∑ j ∈ s, fun₀ | j => 1)) 1) t) <
    supDegree (⇑toLex) ((fun s => (monomial (∑ j ∈ s, fun₀ | j => 1)) 1) (Iic ⟨i, him⟩))

Tactic:
simp_rw [← single_eq_monomial, supDegree_single_ne_zero _ one_ne_zero,
  ← Finsupp.indicator_eq_sum_single]

Result:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ toLex (Finsupp.indicator t fun x x => 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1)

Proof state:
case refine_2.refine_1.hc
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 => x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic ⟨i, him⟩
h : k ∉ t
⊢ False

Tactic:
exact lt_irrefl k <| ((lt_min'_iff _ _).1 hk) _ <| mem_sdiff.2 ⟨hki, h⟩

Result:
no goals

Proof state:
case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ 0 < 1

Tactic:
exact Nat.zero_lt_one

Result:
no goals

Proof state:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : ∃ x ∈ Iic ⟨i, him⟩, x ∉ t
ht' : #t = #(Iic ⟨i, him⟩)
⊢ toLex (Finsupp.indicator t fun x x => 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1)

Tactic:
simp_rw [← mem_sdiff] at hne

Result:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
⊢ toLex (Finsupp.indicator t fun x x => 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1)

Proof state:
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
⊢ #t = #(Iic ⟨i, him⟩)

Tactic:
rw [(mem_powersetCard.1 ht).2, Fin.card_Iic]

Result:
no goals

Proof state:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ toLex (Finsupp.indicator t fun x x => 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1)

Tactic:
refine ⟨min' _ hne, fun k hk ↦ ?_, ?_⟩

Result:
case refine_2.refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 => x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
⊢ (ofLex (toLex (Finsupp.indicator t fun x x => 1))) k =
    (ofLex (toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1))) k

case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ (fun {i} x1 x2 => x1 < x2) ((ofLex (toLex (Finsupp.indicator t fun x x => 1))) ((Iic ⟨i, him⟩ \ t).min' hne))
    ((ofLex (toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1))) ((Iic ⟨i, him⟩ \ t).min' hne))

Proof state:
case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ (fun {i} x1 x2 => x1 < x2) ((ofLex (toLex (Finsupp.indicator t fun x x => 1))) ((Iic ⟨i, him⟩ \ t).min' hne))
    ((ofLex (toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1))) ((Iic ⟨i, him⟩ \ t).min' hne))

Tactic:
simp only [Pi.toLex_apply, ofLex_toLex, Finsupp.indicator_apply]

Result:
case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ (if hi : (Iic ⟨i, him⟩ \ t).min' hne ∈ t then 1 else 0) <
    if hi : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ then 1 else 0

Proof state:
case refine_1
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ Iic ⟨i, him⟩ ∈ powersetCard (i + 1) univ

Tactic:
exact mem_powersetCard.2 ⟨subset_univ _, Fin.card_Iic _⟩

Result:
no goals

Proof state:
case refine_2.refine_1.hc
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 => x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic ⟨i, him⟩
⊢ k ∈ t

Tactic:
by_contra h

Result:
case refine_2.refine_1.hc
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
k : Fin m
hk : (fun x1 x2 => x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic ⟨i, him⟩
h : k ∉ t
⊢ False

Proof state:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
⊢ supDegree (⇑toLex) ((fun s => (monomial (∑ j ∈ s, fun₀ | j => 1)) 1) t) <
    supDegree (⇑toLex) ((fun s => (monomial (∑ j ∈ s, fun₀ | j => 1)) 1) (Iic ⟨i, him⟩))

Tactic:
have ht' : #t = #(Iic (⟨i, him⟩ : Fin m)) := by
  rw [(mem_powersetCard.1 ht).2, Fin.card_Iic]

Result:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ supDegree (⇑toLex) ((fun s => (monomial (∑ j ∈ s, fun₀ | j => 1)) 1) t) <
    supDegree (⇑toLex) ((fun s => (monomial (∑ j ∈ s, fun₀ | j => 1)) 1) (Iic ⟨i, him⟩))