A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
e : W ⟶ cokernel f
he : e ≫ cokernel.desc f g w = 0
⊢ (kernel.lift (cokernel.desc f g w) e he ≫ (homologyIsoKernelDesc f g w).inv) ≫
      (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    e
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
W : A
e : W ⟶ cokernel f
he : e ≫ cokernel.desc f g w = 0
⊢ lift f g w e he ≫ ι f g w = e
dsimp [ι, lift]
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
W : A
e : W ⟶ cokernel f
he : e ≫ cokernel.desc f g w = 0
⊢ (kernel.lift (cokernel.desc f g w) e he ≫ (homologyIsoKernelDesc f g w).inv) ≫
      (homologyIsoKernelDesc f g w).hom ≫ kernel.ι (cokernel.desc f g w) =
    e
simp