J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ lift F t.cone ≫ π F j = t.cone.π.app j
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).inv ≫ π F j = t.cone.π.app j
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
no goals
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F✝ F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ lift F t.cone ≫ π F j = t.cone.π.app j
aesop_cat