no goals
α : Type u_1
β : Type ?u.12507
γ : Type ?u.12510
δ : Type ?u.12513
ι : Sort ?u.12516
κ : ι → Sort ?u.12521
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
s t : NonemptyInterval α
x : α × α
a b : α
⊢ b ∈ pure a ↔ b = a
rw [← SetLike.mem_coe, coe_pure, mem_singleton_iff]