case intro.intro
α : Type u_1
β : Type ?u.23495
γ : Type ?u.23498
ι : Sort ?u.23501
κ : ι → Sort ?u.23506
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a✝ : α
inst✝ : NoMinOrder α
hs : IsLowerSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ lowerBounds s
⊢ False
α : Type u_1
β : Type ?u.23495
γ : Type ?u.23498
ι : Sort ?u.23501
κ : ι → Sort ?u.23506
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a : α
inst✝ : NoMinOrder α
hs : IsLowerSet s
⊢ Set.Nonempty s → ¬BddBelow s
rintro ⟨a, ha⟩ ⟨b, hb⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.23495
γ : Type ?u.23498
ι : Sort ?u.23501
κ : ι → Sort ?u.23506
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a✝ : α
inst✝ : NoMinOrder α
hs : IsLowerSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ lowerBounds s
c : α
hc : c < b
⊢ False
case intro.intro
α : Type u_1
β : Type ?u.23495
γ : Type ?u.23498
ι : Sort ?u.23501
κ : ι → Sort ?u.23506
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a✝ : α
inst✝ : NoMinOrder α
hs : IsLowerSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ lowerBounds s
⊢ False
obtain ⟨c, hc⟩ := exists_lt b
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.23495
γ : Type ?u.23498
ι : Sort ?u.23501
κ : ι → Sort ?u.23506
inst✝² : Preorder α
inst✝¹ : Preorder β
s : Set α
p : α → Prop
a✝ : α
inst✝ : NoMinOrder α
hs : IsLowerSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ lowerBounds s
c : α
hc : c < b
⊢ False
exact hc.not_le (hb <| hs (hc.le.trans <| hb ha) ha)