case w
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
J : Type w
inst✝³ : Category J
F : J ⥤ C
inst✝² : PreservesLimit F G
inst✝¹ : HasLimit F
inst✝ : HasLimit (F ⋙ G)
t : Cone F
j✝ : J
⊢ (G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom) ≫ limit.π (F ⋙ G) j✝ =
    limit.lift (F ⋙ G) (G.mapCone t) ≫ limit.π (F ⋙ G) j✝
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
J : Type w
inst✝³ : Category J
F : J ⥤ C
inst✝² : PreservesLimit F G
inst✝¹ : HasLimit F
inst✝ : HasLimit (F ⋙ G)
t : Cone F
⊢ G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom = limit.lift (F ⋙ G) (G.mapCone t)
ext
no goals
case w
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
G : C ⥤ D
J : Type w
inst✝³ : Category J
F : J ⥤ C
inst✝² : PreservesLimit F G
inst✝¹ : HasLimit F
inst✝ : HasLimit (F ⋙ G)
t : Cone F
j✝ : J
⊢ (G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom) ≫ limit.π (F ⋙ G) j✝ =
    limit.lift (F ⋙ G) (G.mapCone t) ≫ limit.π (F ⋙ G) j✝
simp [← G.map_comp]