no goals
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0
simp only [← G.map_comp, w, Functor.map_zero]
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ coequalizer.π (G.map f) 0 ≫ cokernelComparison f G ≫ G.map (cokernel.desc f h w) =
    coequalizer.π (G.map f) 0 ≫ cokernel.desc (G.map f) (G.map h) (_ : G.map f ≫ G.map h = 0)
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ cokernelComparison f G ≫ G.map (cokernel.desc f h w) = cokernel.desc (G.map f) (G.map h) (_ : G.map f ≫ G.map h = 0)
apply coequalizer.hom_ext
no goals
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ coequalizer.π (G.map f) 0 ≫ cokernelComparison f G ≫ G.map (cokernel.desc f h w) =
    coequalizer.π (G.map f) 0 ≫ cokernel.desc (G.map f) (G.map h) (_ : G.map f ≫ G.map h = 0)
simp [← G.map_comp]