no goals
C : Type u
inst✝³ : Category C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ G.map f ≫ G.map h = G.map g ≫ G.map h
simp only [← G.map_comp, w]
case h
C : Type u
inst✝³ : Category C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
    coequalizer.π (G.map f) (G.map g) ≫ coequalizer.desc (G.map h) (_ : G.map f ≫ G.map h = G.map g ≫ G.map h)
C : Type u
inst✝³ : Category C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
    coequalizer.desc (G.map h) (_ : G.map f ≫ G.map h = G.map g ≫ G.map h)
apply coequalizer.hom_ext
no goals
case h
C : Type u
inst✝³ : Category C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
    coequalizer.π (G.map f) (G.map g) ≫ coequalizer.desc (G.map h) (_ : G.map f ≫ G.map h = G.map g ≫ G.map h)
simp [← G.map_comp]