no goals
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
c₁ c₂ : Cone F
t : IsLimit c₁
⊢ ∀ (j : J), G.map (IsLimit.lift t c₂) ≫ (G.mapCone c₁).π.app j = (G.mapCone c₂).π.app j
simp [← G.map_comp]