no goals
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W✝ X Y Z : C
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k
simp only [← G.map_comp, w]
no goals
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W✝ X Y Z : C
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushoutComparison G f g ≫ G.map (pushout.desc h k w) =
    pushout.desc (G.map h) (G.map k) (_ : G.map f ≫ G.map h = G.map g ≫ G.map k)
ext <;> simp [← G.map_comp]