mathlib3

9b255781 - fix(category_theory/limits): avoid a rewrite in a definition (#2458)

fix(category_theory/limits): avoid a rewrite in a definition (#2458) The proof that every equalizer of `f` and `g` is an isomorphism if `f = g` had an ugly rewrite in a definition (introduced by yours truly). This PR reformulates the proof in a cleaner way by working with two morphisms `f` and `g` and a proof of `f = g` right from the start, which is easy to specialze to the case `(f, f)`, instead of trying to reduce the `(f, g)` case to the `(f, f)` case by rewriting. This also lets us get rid of `fork.eq_of_ι_ι`, unless someone wants to keep it, but personally I don't think that using it is ever a good idea.