ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
⊢ sSup s ∈ s
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
⊢ IsSupClosedCompact α
intro s hne hsc
case intro.intro
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ sSup s ∈ s
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
⊢ sSup s ∈ s
obtain ⟨t, ht₁, ht₂⟩ := h s
case intro.intro
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ sSup s ∈ s
case intro.intro
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : IsSupFiniteCompact α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ sSup s ∈ s
clear h
case intro.intro.inl
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : t = ∅
⊢ sSup s ∈ s

case intro.intro.inr
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : Finset.Nonempty t
⊢ sSup s ∈ s
case intro.intro
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ sSup s ∈ s
cases' t.eq_empty_or_nonempty with h h
case intro.intro.inl
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = Finset.sup ∅ id
⊢ sSup s ∈ s
case intro.intro.inl
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : t = ∅
⊢ sSup s ∈ s
subst h
case intro.intro.inl
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s
case intro.intro.inl
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = Finset.sup ∅ id
⊢ sSup s ∈ s
rw [Finset.sup_empty] at ht₂
case intro.intro.inl
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s
case intro.intro.inl
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s
rw [ht₂]
no goals
case intro.intro.inl
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s
simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]
case intro.intro.inr
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : Finset.Nonempty t
⊢ Finset.sup t id ∈ s
case intro.intro.inr
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : Finset.Nonempty t
⊢ sSup s ∈ s
rw [ht₂]
no goals
case intro.intro.inr
ι : Sort ?u.26576
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
s : Set α
hne : Set.Nonempty s
hsc : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a ⊔ b ∈ s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
h : Finset.Nonempty t
⊢ Finset.sup t id ∈ s
exact t.sup_closed_of_sup_closed h ht₁ hsc