no goals
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F✝ : J ⥤ C
t✝ : Cone F✝
F G : J ⥤ C
r s : Cone G
t : Cone F
P : IsLimit t
Q : IsLimit s
w : F ≅ G
⊢ ∀ (j : J), (lift Q r ≫ (conePointsIsoOfNatIso P Q w).inv) ≫ t.π.app j = map r P w.inv ≫ t.π.app j
simp