case intro.intro
α : Type u_1
β : Type ?u.22760
γ : Type ?u.22763
ι : Sort ?u.22766
κ : ι → Sort ?u.22771
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a✝ : α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
⊢ False
α : Type u_1
β : Type ?u.22760
γ : Type ?u.22763
ι : Sort ?u.22766
κ : ι → Sort ?u.22771
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a : α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
⊢ Set.Nonempty s → ¬BddAbove s
rintro ⟨a, ha⟩ ⟨b, hb⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.22760
γ : Type ?u.22763
ι : Sort ?u.22766
κ : ι → Sort ?u.22771
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a✝ : α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
c : α
hc : b < c
⊢ False
case intro.intro
α : Type u_1
β : Type ?u.22760
γ : Type ?u.22763
ι : Sort ?u.22766
κ : ι → Sort ?u.22771
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a✝ : α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
⊢ False
obtain ⟨c, hc⟩ := exists_gt b
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.22760
γ : Type ?u.22763
ι : Sort ?u.22766
κ : ι → Sort ?u.22771
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a✝ : α
inst✝ : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
c : α
hc : b < c
⊢ False
exact hc.not_le (hb <| hs ((hb ha).trans hc.le) ha)