mathlib3

7b5c60db - feat(data/equiv/basic): add a small lemma for simplifying map between equivalent quotient spaces induced by equivalent relations (#8617)

feat(data/equiv/basic): add a small lemma for simplifying map between equivalent quotient spaces induced by equivalent relations (#8617) Just adding a small lemma that allows us to compute the composition of the map given by `quot.congr` with `quot.mk`