-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem IsSupFiniteCompact.isSupClosedCompact (h : IsSupFiniteCompact α) :
    IsSupClosedCompact α

Proof state:
case intro.intro.inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t = ∅
⊢ sSup s ∈ s

Tactic:
subst h

Result:
case intro.intro.inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ∅.sup id
⊢ sSup s ∈ s

Proof state:
case intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s

Tactic:
clear h

Result:
case intro.intro
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s

Proof state:
case intro.intro.inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ t.sup id ∈ s

Tactic:
exact hsc.finsetSup_mem h ht₁

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
⊢ sSup s ∈ s

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := h s

Result:
case intro.intro
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s

Proof state:
case intro.intro.inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ∅.sup id
⊢ sSup s ∈ s

Tactic:
rw [Finset.sup_empty] at ht₂

Result:
case intro.intro.inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s

Proof state:
case intro.intro.inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s

Tactic:
rw [ht₂]

Result:
case intro.intro.inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s

Proof state:
case intro.intro.inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s

Tactic:
rw [ht₂]

Result:
case intro.intro.inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ t.sup id ∈ s

Proof state:
case intro.intro.inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : ↑∅ ⊆ s
ht₂ : sSup s = ⊥
⊢ ⊥ ∈ s

Tactic:
simp [eq_singleton_bot_of_sSup_eq_bot_of_nonempty ht₂ hne]

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s

Tactic:
rcases t.eq_empty_or_nonempty with h | h

Result:
case intro.intro.inl
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t = ∅
⊢ sSup s ∈ s

case intro.intro.inr
α : Type u_2
inst✝ : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
⊢ IsSupClosedCompact α

Tactic:
intro s hne hsc

Result:
α : Type u_2
inst✝ : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
⊢ sSup s ∈ s