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.