case inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB s (sSup s)

case inr
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : Set.Nonempty s
⊢ IsLUB s (sSup s)
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsLUB s (sSup s)
cases' s.eq_empty_or_nonempty with hs hs
no goals
case inr
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : Set.Nonempty s
⊢ IsLUB s (sSup s)
exact isLUB_sSup' hs
case inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (sSup ∅)
case inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB s (sSup s)
rw [hs]
case inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (if ⊤ ∈ ∅ then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' ∅) then ↑(sSup ((fun a => ↑a) ⁻¹' ∅)) else ⊤)
case inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (sSup ∅)
dsimp only [sSup]
case inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (if ⊤ ∈ ∅ then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' ∅) then ↑(sSup ((fun a => ↑a) ⁻¹' ∅)) else ⊤)
case inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (if ⊤ ∈ ∅ then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' ∅) then ↑(sSup ((fun a => ↑a) ⁻¹' ∅)) else ⊤)
show IsLUB ∅ _
case inl.inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∈ ∅
⊢ IsLUB ∅ ⊤

case inl.inr.inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ↑(sSup ((fun a => ↑a) ⁻¹' ∅))

case inl.inr.inr
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ⊤
case inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (if ⊤ ∈ ∅ then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' ∅) then ↑(sSup ((fun a => ↑a) ⁻¹' ∅)) else ⊤)
split_ifs with h₁ h₂
no goals
case inl.inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∈ ∅
⊢ IsLUB ∅ ⊤
cases h₁
case inl.inr.inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ↑⊥
case inl.inr.inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ↑(sSup ((fun a => ↑a) ⁻¹' ∅))
rw [preimage_empty, csSup_empty]
no goals
case inl.inr.inl
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ↑⊥
exact isLUB_empty
case inl.inr.inr.h
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ False
case inl.inr.inr
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ⊤
exfalso
case inl.inr.inr.h
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ BddAbove ((fun a => ↑a) ⁻¹' ∅)
case inl.inr.inr.h
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ False
apply h₂
case inl.inr.inr.h
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ ⊥ ∈ upperBounds ((fun a => ↑a) ⁻¹' ∅)
case inl.inr.inr.h
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ BddAbove ((fun a => ↑a) ⁻¹' ∅)
use ⊥
no goals
case inl.inr.inr.h
α : Type u_1
β : Type ?u.88320
γ : Type ?u.88323
ι : Sort ?u.88326
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ¬⊤ ∈ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ ⊥ ∈ upperBounds ((fun a => ↑a) ⁻¹' ∅)
rintro a ⟨⟩