mathlib3

7929a63e - feat(set_theory/zfc): more `quotient` lemmas (#15324)

feat(set_theory/zfc): more `quotient` lemmas (#15324) It seems like we decided to use a custom `mk` definition for `Set` instead of `quotient.mk`. As such, we transfer the basic results on quotients to `Set`, in order to aid rewriting.