C : Type u₁
inst✝⁷ : Category C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G
C : Type u₁
inst✝⁷ : Category C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ (iso G f).inv = cokernelComparison f G
rw [← cancel_epi (cokernel.π _)]
no goals
C : Type u₁
inst✝⁷ : Category C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : Functor.PreservesZeroMorphisms G
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G
simp [PreservesCokernel.iso]