no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι f.op).unop = eqToHom (_ : Y.op.unop = Y) ≫ cokernel.π f ≫ (kernelOpUnop f).inv
simp [kernelOpUnop]