case refine'_1
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id

case refine'_2
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
refine' ⟨fun h k s hs => _, fun h s => _⟩
case refine'_1.intro.intro
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case refine'_1
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
obtain ⟨t, ⟨hts, htsup⟩⟩ := h s
case refine'_1.intro.intro
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = Finset.sup t id
⊢ k ≤ Finset.sup t id
case refine'_1.intro.intro
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
use t, hts
no goals
case refine'_1.intro.intro
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s = Finset.sup t id
⊢ k ≤ Finset.sup t id
rwa [← htsup]
case refine'_2.intro.intro
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
case refine'_2
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
obtain ⟨t, ⟨hts, htsup⟩⟩ := h (sSup s) s (by rfl)
case refine'_2.intro.intro
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
this : sSup s = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
case refine'_2.intro.intro
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
have : sSup s = t.sup id := by
  suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
  simp only [id.def, Finset.sup_le_iff]
  intro x hx
  exact le_sSup _ _ (hts hx)
no goals
case refine'_2.intro.intro
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
this : sSup s = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
exact ⟨t, hts, this⟩
no goals
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
⊢ sSup s ≤ sSup s
rfl
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ Finset.sup t id ≤ sSup s
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ sSup s = Finset.sup t id
suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ ∀ (b : α), b ∈ t → b ≤ sSup s
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ Finset.sup t id ≤ sSup s
simp only [id.def, Finset.sup_le_iff]
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
x : α
hx : x ∈ t
⊢ x ≤ sSup s
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
⊢ ∀ (b : α), b ∈ t → b ≤ sSup s
intro x hx
no goals
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
x : α
hx : x ∈ t
⊢ x ≤ sSup s
exact le_sSup _ _ (hts hx)
no goals
ι : Sort ?u.75433
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : ∀ (k : α), IsCompactElement k
s : Set α
t : Finset α
hts : ↑t ⊆ s
htsup : sSup s ≤ Finset.sup t id
this : Finset.sup t id ≤ sSup s
⊢ sSup s = Finset.sup t id
apply le_antisymm <;> assumption