fix(algebra/category/*/colimits): cleaning up (#2469)
With the passage of time, it seems some difficulties have dissolved away, and steps in the semi-automated construction of colimits in algebraic categories which previously required `rw` or even `erw`, can now be handled by `simp`. Yay!
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
