no goals
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
G : C ⥤ D
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = g ≫ h
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv = coequalizer.π (G.map f) (G.map g)
rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
  comp_id]