no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b✝ : α
s : Set α
b c : α
H₁ : Set.Nonempty (Iio c)
H₂ : b ≤ c
⊢ b ∈ closure (Iio c)
rwa [closure_Iio' H₁]