no goals
C : Type u_1
inst✝¹ : Category C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i
simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w