-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem isSupFiniteCompact_iff_all_elements_compact :
    IsSupFiniteCompact α ↔ ∀ k : α, IsCompactElement k

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
⊢ sSup s ≤ sSup s

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
obtain ⟨t, ⟨hts, htsup⟩⟩ := h s

Result:
case refine_1.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ sSup s = t.sup id

Tactic:
suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ t.sup id ≤ sSup s

Proof state:
case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
obtain ⟨t, ⟨hts, htsup⟩⟩ := h (sSup s) s (by rfl)

Result:
case refine_2.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
x : α
hx : x ∈ t
⊢ x ≤ sSup s

Tactic:
exact le_sSup _ _ (hts hx)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ ∀ b ∈ t, b ≤ sSup s

Tactic:
intro x hx

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
x : α
hx : x ∈ t
⊢ x ≤ sSup s

Proof state:
case refine_1.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
use t, hts

Result:
case right
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = t.sup id
⊢ k ≤ t.sup id

Proof state:
case refine_2.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : sSup s = t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
exact ⟨t, hts, this⟩

Result:
no goals

Proof state:
case right
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = t.sup id
⊢ k ≤ t.sup id

Tactic:
rwa [← htsup]

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Tactic:
have : sSup s = t.sup id := by
  suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
  simp only [id, Finset.sup_le_iff]
  intro x hx
  exact le_sSup _ _ (hts hx)

Result:
case refine_2.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : sSup s = t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ sSup s = t.sup id

Tactic:
apply le_antisymm <;> assumption

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k

Tactic:
refine ⟨fun h k s hs => ?_, fun h s => ?_⟩

Result:
case refine_1
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

case refine_2
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = t.sup id

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ t.sup id ≤ sSup s

Tactic:
simp only [id, Finset.sup_le_iff]

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ t.sup id
⊢ ∀ b ∈ t, b ≤ sSup s