mathlib3

cd0d8c02 - chore(category_theory/limits/over): generalise, golf and document over limits (#5674)

chore(category_theory/limits/over): generalise, golf and document over limits (#5674) - Show that the forgetful functor `over X => C` creates colimits, generalising what was already there - Golf the proofs using this new instance - Add module doc and duals of the above