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