J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasLimit F
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
⊢ HasLimit F
haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimitEquivalenceComp e.symm
no goals
J : Type u₁
inst✝³ : Category J
K : Type u₂
inst✝² : Category K
C : Type u
inst✝¹ : Category C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasLimit F
apply hasLimitOfIso (e.invFunIdAssoc F)