no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
r s t : Cocone F
P : IsColimit s
Q : IsColimit t
⊢ ∀ (j : J), t.ι.app j ≫ (coconePointUniqueUpToIso P Q).inv ≫ desc P r = r.ι.app j
simp