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 : Cone F
P : IsLimit s
Q : IsLimit t
⊢ ∀ (j : J), (lift P r ≫ (conePointUniqueUpToIso P Q).hom) ≫ t.π.app j = r.π.app j
simp