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
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g
rw [← G.map_comp, hpq, G.map_comp]
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
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ (PreservesCokernel.iso G f).hom ≫
      cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) (_ : G.map f ≫ G.map q = G.map p ≫ G.map g) =
    G.map (cokernel.map f g p q hpq) ≫ (PreservesCokernel.iso G g).hom
rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
  cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]