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
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ IsLimit.lift (limit.isLimit G)
        ((Cones.equivalenceOfReindexing (Equivalence.symm e)
                ((isoWhiskerLeft e.inverse w).symm ≪≫ Equivalence.invFunIdAssoc e G)).functor.obj
          (limit.cone F)) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map ((Equivalence.counit e).app k)
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
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (isoOfEquivalence e w).hom ≫ limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map ((Equivalence.counit e).app k)
simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
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
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ limit.lift G
        ((Cones.postcompose (whiskerLeft e.inverse w.inv ≫ (Equivalence.invFunIdAssoc e G).hom)).obj
          (Cone.whisker e.inverse (limit.cone F))) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map ((Equivalence.counit e).app k)
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
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ IsLimit.lift (limit.isLimit G)
        ((Cones.equivalenceOfReindexing (Equivalence.symm e)
                ((isoWhiskerLeft e.inverse w).symm ≪≫ Equivalence.invFunIdAssoc e G)).functor.obj
          (limit.cone F)) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map ((Equivalence.counit e).app k)
dsimp
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
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ limit.lift G
        ((Cones.postcompose (whiskerLeft e.inverse w.inv ≫ (Equivalence.invFunIdAssoc e G).hom)).obj
          (Cone.whisker e.inverse (limit.cone F))) ≫
      limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map ((Equivalence.counit e).app k)
simp