feat(category_theory/kernels): kernel_iso_of_eq (#3372)
This provides two useful isomorphisms when working with abstract (co)kernels:
```
def kernel_zero_iso_source [has_kernel (0 : X ⟶ Y)] : kernel (0 : X ⟶ Y) ≅ X :=
def kernel_iso_of_eq {f g : X ⟶ Y} [has_kernel f] [has_kernel g] (h : f = g) : kernel f ≅ kernel g :=
```
and some associated simp lemmas.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
