refactor(category_theory/limits/types): Refactor filtered colimits. (#9100)
refactor(category_theory/limits/types): Refactor filtered colimits. (#9100)

- Rename `filtered_colimit.r` into `filtered_colimit.rel`, to match up with `quot.rel`,
- Rename lemma `r_ge`,
- Abstract out lemma `eqv_gen_quot_rel_of_rel` from later proof.





leanprover-community/mathlib,leanprover-community/mathlib