no goals
α : Type u_1
β : Type ?u.29168
γ : Type ?u.29171
δ : Type ?u.29174
ι : Sort ?u.29177
κ : ι → Sort ?u.29182
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
s t : Interval α
a b : α
⊢ b ∈ pure a ↔ b = a
rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]