Equivalence class of a setoid

Stream: Is there code for X?

[Heather Macbeth]

Given a quotient, I'd like to get my hands on the preimage of a particular point in the quotient, and a couple of simple lemmas about it. Is this in mathlib somewhere?

import data.set.basic

variables {α : Type*} {s : setoid α}

def quotient.set (q : quotient s) : set α := quotient.mk ⁻¹' {q}

lemma quotient.nonempty_set (q : quotient s) : q.set.nonempty :=
q.exists_rep

lemma quotient.mem_set (q : quotient s) {a₀ : α} (ha : a₀ ∈ q.set) :
  q.set = {a : α | setoid.r a a₀} :=
begin
  ext a,
  rw (ha.symm : q = ⟦a₀⟧),
  exact quotient.eq,
end

[Adam Topaz]

If it's anywhere it would be around docs#setoid.classes

[Heather Macbeth]

Yes, I just noticed docs#setoid.classes, so maybe another way of phrasing it is, does mathlib have written down the canonical equiv from s.classes to quotient s?

[Adam Topaz]

docs#indexed_partition.equiv_quotient

[Adam Topaz]

I don't see a version using docs#setoid.is_partition though