A type with an equivalence relation on it is called a setoid in Lean. Setoids are defined in init/data/setoid.lean and the quotient type corresponding to the equivalence classes of the equivalence relation is defined in init/data/quot.lean . The online document Theorem Proving In Lean has quite a good section about setoids and quotients[external link].
TODO: find a nice equivalence relation in mathlib (quotient groups? congruences mod n?) and give it as an example here.
Xena 