mem_iff for subsingletons

Stream: Is there code for X?

[Yaël Dillies]

Do we already have this simple lemma somewhere?

@[simp] lemma set.mem_iff_nonempty_of_subsingleton {α : Type*} [subsingleton α] {s : set α}
  {x : α} :
  x ∈ s ↔ s.nonempty :=
begin
  refine ⟨λ hx, ⟨x, hx⟩, _⟩,
  rintro ⟨y, hy⟩,
  rwa subsingleton.elim x y,
end

[Scott Morrison]

It's not super clear this should be a simp lemma.