no goals
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ ι s = l ≫ ι s
this : k ≫ ι s ≫ f = l ≫ ι s ≫ f
⊢ k ≫ s.π.app one = l ≫ s.π.app one
rw [s.app_one_eq_ι_comp_left, this]
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ ι s = l ≫ ι s
⊢ (k ≫ ι s) ≫ f = (l ≫ ι s) ≫ f
C : Type u
inst✝ : Category C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ ι s = l ≫ ι s
⊢ k ≫ ι s ≫ f = l ≫ ι s ≫ f
simp only [← Category.assoc]