no goals
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
s : Cofork f g
W : C
k l : s.pt ⟶ W
h : π s ≫ k = π s ≫ l
⊢ s.ι.app zero ≫ k = s.ι.app zero ≫ l
simp only [s.app_zero_eq_comp_π_left, Category.assoc, h]