case pos
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
hx : IsBot x
⊢ ∃ y, y ∈ s ∧ y ≤ x

case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
hx : ¬IsBot x
⊢ ∃ y, y ∈ s ∧ y ≤ x
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
⊢ ∃ y, y ∈ s ∧ y ≤ x
by_cases hx : IsBot x
no goals
case pos
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
hx : IsBot x
⊢ ∃ y, y ∈ s ∧ y ≤ x
exact ⟨x, hbot x hx, le_rfl⟩
case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
hx : ∃ x_1, x_1 < x
⊢ ∃ y, y ∈ s ∧ y ≤ x
case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
hx : ¬IsBot x
⊢ ∃ y, y ∈ s ∧ y ≤ x
simp only [IsBot, not_forall, not_le] at hx
case neg.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
hx : ∃ x_1, x_1 < x
y : α
hys : y ∈ s
hy : y < x
⊢ ∃ y, y ∈ s ∧ y ≤ x
case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
hx : ∃ x_1, x_1 < x
⊢ ∃ y, y ∈ s ∧ y ≤ x
rcases hs.exists_mem_open isOpen_Iio hx with ⟨y, hys, hy : y < x⟩
no goals
case neg.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
s : Set α
hs : Dense s
hbot : ∀ (x : α), IsBot x → x ∈ s
x : α
hx : ∃ x_1, x_1 < x
y : α
hys : y ∈ s
hy : y < x
⊢ ∃ y, y ∈ s ∧ y ≤ x
exact ⟨y, hys, hy.le⟩