no goals
J : Type w
C : Type u
inst✝¹ : Category C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Cotrident f
W : C
k l : s.pt ⟶ W
h : π s ≫ k = π s ≫ l
⊢ s.ι.app zero ≫ k = s.ι.app zero ≫ l
rw [← s.app_one (Classical.arbitrary J), Category.assoc, Category.assoc, h]