no goals
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F : J ⥤ C
inst✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ : HasLimit (D ⋙ E ⋙ F)
s : LimitCone (E ⋙ F)
t : LimitCone F
⊢ pre F E = (isoLimitCone t).hom ≫ IsLimit.lift s.isLimit (Cone.whisker E t.cone) ≫ (isoLimitCone s).inv
aesop_cat