no goals
C : Type u
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
W✝ X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : inl t ≫ k = inl t ≫ l
h₁ : inr t ≫ k = inr t ≫ l
⊢ t.ι.app none ≫ k = t.ι.app none ≫ l
rw [← t.w fst, Category.assoc, Category.assoc, h₀]