-- 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
⊢ ∀ j ∈ powersetCard (i + 1) univ,
    j ≠ Iic ⟨i, him⟩ →
      supDegree (⇑toLex) ((fun s => (monomial (∑ j ∈ s, fun₀ | j => 1)) 1) j) <
        supDegree (⇑toLex) ((fun s => (monomial (∑ j ∈ s, fun₀ | j => 1)) 1) (Iic ⟨i, him⟩))

Tactic:
intro t ht 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
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⟩))

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
⊢ (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

Tactic:
rw [dif_neg hkm.2, dif_pos hkm.1]

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
⊢ 0 < 1

Proof state:
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)
⊢ (if hi : k ∈ t then 1 else 0) = if hi : k ∈ Iic ⟨i, him⟩ then 1 else 0

Tactic:
have hki := mem_Iic.2 (hk.le.trans <| mem_Iic.1 hkm.1)

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)
hki : k ∈ Iic ⟨i, him⟩
⊢ (if hi : k ∈ t then 1 else 0) = if hi : k ∈ Iic ⟨i, him⟩ then 1 else 0

Proof state:
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
⊢ supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1) ∧
    Monic (⇑toLex) (esymm (Fin m) R (i + 1))

Tactic:
have := supDegree_leadingCoeff_sum_eq (D := toLex) (s := univ.powersetCard (i + 1))
  (i := Iic (⟨i, him⟩ : Fin m)) ?_ (f := fun s ↦ monomial (∑ j ∈ s, fun₀ | j => 1) (1 : R)) ?_

Result:
case refine_3
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
this :
  supDegree (⇑toLex) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      supDegree (⇑toLex) ((monomial (∑ j ∈ Iic ⟨i, him⟩, fun₀ | j => 1)) 1) ∧
    leadingCoeff (⇑toLex) (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1)) 1) =
      leadingCoeff (⇑toLex) ((monomial (∑ j ∈ Iic ⟨i, him⟩, fun₀ | j => 1)) 1)
⊢ supDegree (⇑toLex) (esymm (Fin m) R (i + 1)) = toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1) ∧
    Monic (⇑toLex) (esymm (Fin m) R (i + 1))

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

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

Proof state:
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)
hki : k ∈ Iic ⟨i, him⟩
⊢ (if hi : k ∈ t then 1 else 0) = if hi : k ∈ Iic ⟨i, him⟩ then 1 else 0

Tactic:
rw [dif_pos hki, dif_pos]

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⟩
⊢ k ∈ t

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⟩)
⊢ toLex (Finsupp.indicator t fun x x => 1) < toLex (Finsupp.indicator (Iic ⟨i, him⟩) fun x x => 1)

Tactic:
rw [ne_comm, Ne, ← subset_iff_eq_of_card_le ht'.le, not_subset] 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
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)

Proof state:
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))

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

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)
⊢ (if hi : k ∈ t then 1 else 0) = if hi : k ∈ Iic ⟨i, him⟩ then 1 else 0

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