-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem WellFoundedGT.isSupFiniteCompact [WellFoundedGT α] :
    IsSupFiniteCompact α := fun s => by
  let S := { x | ∃ t : Finset α, ↑t ⊆ s ∧ t.sup id = x }
  obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := wellFounded_gt.has_min S ⟨⊥, ∅, by simp⟩
  refine ⟨t, ht₁, (sSup_le _ _ fun y hy => ?_).antisymm ?_⟩
  · classical
    rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
    simp
  · rw [Finset.sup_id_eq_sSup]
    exact sSup_le_sSup ht₁

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
let S := { x | ∃ t : Finset α, ↑t ⊆ s ∧ t.sup id = x }

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
y : α
hy : y ∈ s
⊢ y ≤ t.sup id

Tactic:
rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
    (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]

Result:
case intro.intro.intro.intro.refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
y : α
hy : y ∈ s
⊢ y ≤ (insert y t).sup id

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
⊢ t.sup id ≤ sSup s

Tactic:
rw [Finset.sup_id_eq_sSup]

Result:
case intro.intro.intro.intro.refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
⊢ sSup ↑t ≤ sSup s

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
⊢ sSup ↑t ≤ sSup s

Tactic:
exact sSup_le_sSup ht₁

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := wellFounded_gt.has_min S ⟨⊥, ∅, by simp⟩

Result:
case intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
⊢ ↑∅ ⊆ s ∧ ∅.sup id = ⊥

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
refine ⟨t, ht₁, (sSup_le _ _ fun y hy => ?_).antisymm ?_⟩

Result:
case intro.intro.intro.intro.refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
y : α
hy : y ∈ s
⊢ y ≤ t.sup id

case intro.intro.intro.intro.refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
⊢ t.sup id ≤ sSup s

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
y : α
hy : y ∈ s
⊢ y ≤ t.sup id

Tactic:
classical
rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
    (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
y : α
hy : y ∈ s
⊢ y ≤ (insert y t).sup id

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬x > t.sup id
y : α
hy : y ∈ s
⊢ ↑(insert y t) ⊆ s ∧ (insert y t).sup id = (insert y t).sup id

Tactic:
simp [Set.insert_subset_iff, hy, ht₁]

Result:
no goals