A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ ((homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)) ≫ cokernel.desc f g w = 0
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ ι f g w ≫ cokernel.desc f g w = 0
dsimp [ι]
no goals
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ ((homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w)) ≫ cokernel.desc f g w = 0
simp