no goals
C : Type u
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
W✝ X Y Z : C
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
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 ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ G.map (pullback.lift h k w) ≫ pullbackComparison G f g =
    pullback.lift (G.map h) (G.map k) (_ : G.map h ≫ G.map f = G.map k ≫ G.map g)
ext <;> simp [← G.map_comp]