case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
x : WithTop α
⊢ x ∈ range some ↔ x ∈ Iio ⊤
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ range some = Iio ⊤
ext x
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
x : WithTop α
⊢ (∃ y, ↑y = x) ↔ ∃ x_1, Option.some x_1 = x
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
x : WithTop α
⊢ x ∈ range some ↔ x ∈ Iio ⊤
rw [mem_Iio, lt_top_iff_ne_top, mem_range, ← none_eq_top, Option.ne_none_iff_exists]
no goals
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
x : WithTop α
⊢ (∃ y, ↑y = x) ↔ ∃ x_1, Option.some x_1 = x
rfl