-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem isLUB_sSup (s : Set (WithTop α)) : IsLUB s (sSup s)

Proof state:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ↑⊥

Tactic:
exact isLUB_empty

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ↑(sSup ((fun a => ↑a) ⁻¹' ∅))

Tactic:
rw [preimage_empty, csSup_empty]

Result:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ↑⊥

Proof state:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∈ ∅
⊢ IsLUB ∅ ⊤

Tactic:
cases h₁

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (sSup ∅)

Tactic:
dsimp only [sSup]

Result:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (if ⊤ ∈ ∅ then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' ∅) then ↑(sSup ((fun a => ↑a) ⁻¹' ∅)) else ⊤)

Proof state:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (if ⊤ ∈ ∅ then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' ∅) then ↑(sSup ((fun a => ↑a) ⁻¹' ∅)) else ⊤)

Tactic:
split_ifs with h₁ h₂

Result:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∈ ∅
⊢ IsLUB ∅ ⊤

case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ↑(sSup ((fun a => ↑a) ⁻¹' ∅))

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ⊤

Proof state:
case h
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ ⊥ ∈ upperBounds ((fun a => ↑a) ⁻¹' ∅)

Tactic:
rintro a ⟨⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB s (sSup s)

Tactic:
rw [hs]

Result:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB ∅ (sSup ∅)

Proof state:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ IsLUB ∅ ⊤

Tactic:
exfalso

Result:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ False

Proof state:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ False

Tactic:
apply h₂

Result:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ BddAbove ((fun a => ↑a) ⁻¹' ∅)

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsLUB s (sSup s)

Tactic:
rcases s.eq_empty_or_nonempty with hs | hs

Result:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
⊢ IsLUB s (sSup s)

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Proof state:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
exact isLUB_sSup' hs

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ BddAbove ((fun a => ↑a) ⁻¹' ∅)

Tactic:
use ⊥

Result:
case h
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : s = ∅
h₁ : ⊤ ∉ ∅
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' ∅)
⊢ ⊥ ∈ upperBounds ((fun a => ↑a) ⁻¹' ∅)