-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem isLUB_sSup' {β : Type*} [ConditionallyCompleteLattice β] {s : Set (WithTop β)}
    (hs : s.Nonempty) : IsLUB s (sSup s)

Proof state:
case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a

Tactic:
exact False.elim (not_top_le_coe a (ha h₁))

Result:
no goals

Proof state:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ∈ lowerBounds (upperBounds s)

Tactic:
rintro (⟨⟩ | b) hb

Result:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ≤ none

case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ≤ Option.some b

Proof state:
case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
⊢ (if ⊤ ∈ s then ⊤ else if BddAbove ((fun a => ↑a) ⁻¹' s) then ↑(sSup ((fun a => ↑a) ⁻¹' s)) else ⊤) ∈ upperBounds s

Tactic:
split_ifs with h₁ h₂

Result:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ upperBounds s

case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ∈ upperBounds s

case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s

Proof state:
case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ b ∈ upperBounds ((fun a => ↑a) ⁻¹' s)

Tactic:
intro a ha

Result:
case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b

Proof state:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ≤ ↑(sSup ((fun a => ↑a) ⁻¹' s))

Tactic:
contradiction

Result:
no goals

Proof state:
case pos.some.refine_1.intro.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b✝ : β
hb✝ : Option.some b✝ ∈ upperBounds s
b : β
hb : Option.some b ∈ s
⊢ ((fun a => ↑a) ⁻¹' s).Nonempty

Tactic:
exact ⟨b, hb⟩

Result:
no goals

Proof state:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ≤ none

Tactic:
exact le_top

Result:
no goals

Proof state:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ ⊤ ≤ none

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ∈ upperBounds s

Tactic:
rintro (⟨⟩ | a) ha

Result:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
ha : none ∈ s
⊢ none ≤ ↑(sSup ((fun a => ↑a) ⁻¹' s))

case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
a : β
ha : Option.some a ∈ s
⊢ Option.some a ≤ ↑(sSup ((fun a => ↑a) ⁻¹' s))

Proof state:
case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ False

Tactic:
apply h₂

Result:
case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ BddAbove ((fun a => ↑a) ⁻¹' s)

Proof state:
case pos.some.refine_1.intro.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb✝ : Option.some b ∈ upperBounds s
hb : none ∈ s
⊢ ((fun a => ↑a) ⁻¹' s).Nonempty

Tactic:
exact absurd hb h₁

Result:
no goals

Proof state:
case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ↑(sSup ((fun a => ↑a) ⁻¹' s)) ≤ Option.some b

Tactic:
refine coe_le_coe.2 (csSup_le ?_ ?_)

Result:
case pos.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ((fun a => ↑a) ⁻¹' s).Nonempty

case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a => ↑a) ⁻¹' s, b_1 ≤ b

Proof state:
case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b

Tactic:
exact coe_le_coe.1 (hb ha)

Result:
no goals

Proof state:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
hb : none ∈ upperBounds s
⊢ ⊤ ≤ none

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s

Tactic:
intro _ _

Result:
case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤

Proof state:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ upperBounds s

Tactic:
intro _ _

Result:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a✝¹ : WithTop β
a✝ : a✝¹ ∈ s
⊢ a✝¹ ≤ ⊤

Proof state:
case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a => ↑a) ⁻¹' s, b_1 ≤ b

Tactic:
intro a ha

Result:
case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
a : β
ha : a ∈ (fun a => ↑a) ⁻¹' s
⊢ a ≤ b

Proof state:
case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ BddAbove ((fun a => ↑a) ⁻¹' s)

Tactic:
use b

Result:
case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a => ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ b ∈ upperBounds ((fun a => ↑a) ⁻¹' s)