[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesLimit F G
c₁ c₂ : Cone F
t : IsLimit c₁
⊢ ∀ (j : J), G.map (IsLimit.lift t c₂) ≫ NatTrans.app (G.mapCone c₁).π j = NatTrans.app (G.mapCone c₂).π j
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} 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)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} 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✝
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
⊢ ∀ {X Y : J ⥤ C} (f : X ⟶ Y),
    (lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y).hom =
      ((fun F => preservesLimitIso G F) X).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f
[PROOFSTEP]
intro _ _ f
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y✝).hom =
    ((fun F => preservesLimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ∀ (j : J),
    ((lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y✝).hom) ≫ limit.π (((whiskeringRight J C D).obj G).obj Y✝) j =
      (((fun F => preservesLimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f) ≫
        limit.π (((whiskeringRight J C D).obj G).obj Y✝) j
[PROOFSTEP]
intro j
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ ((lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y✝).hom) ≫ limit.π (((whiskeringRight J C D).obj G).obj Y✝) j =
    (((fun F => preservesLimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f) ≫
      limit.π (((whiskeringRight J C D).obj G).obj Y✝) j
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ (G.map (limMap f) ≫ (preservesLimitIso G Y✝).hom) ≫ limit.π (Y✝ ⋙ G) j =
    ((preservesLimitIso G X✝).hom ≫ limMap (whiskerRight f G)) ≫ limit.π (Y✝ ⋙ G) j
[PROOFSTEP]
simp only [preservesLimitsIso_hom_π, whiskerRight_app, limMap_π, Category.assoc, preservesLimitsIso_hom_π_assoc, ←
  G.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesColimit F G
c₁ c₂ : Cocone F
t : IsColimit c₁
⊢ ∀ (j : J), NatTrans.app (G.mapCocone c₁).ι j ≫ G.map (IsColimit.desc t c₂) = NatTrans.app (G.mapCocone c₂).ι j
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : PreservesColimit F G
inst✝¹ : HasColimit F
inst✝ : HasColimit (F ⋙ G)
t : Cocone F
⊢ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) = colimit.desc (F ⋙ G) (G.mapCocone t)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : PreservesColimit F G
inst✝¹ : HasColimit F
inst✝ : HasColimit (F ⋙ G)
t : Cocone F
j✝ : J
⊢ colimit.ι (F ⋙ G) j✝ ≫ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) =
    colimit.ι (F ⋙ G) j✝ ≫ colimit.desc (F ⋙ G) (G.mapCocone t)
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
⊢ ∀ {X Y : J ⥤ C} (f : X ⟶ Y),
    (colim ⋙ G).map f ≫ ((fun F => preservesColimitIso G F) Y).hom =
      ((fun F => preservesColimitIso G F) X).hom ≫ ((whiskeringRight J C D).obj G ⋙ colim).map f
[PROOFSTEP]
intro _ _ f
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (colim ⋙ G).map f ≫ ((fun F => preservesColimitIso G F) Y✝).hom =
    ((fun F => preservesColimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ colim).map f
[PROOFSTEP]
rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ((fun F => preservesColimitIso G F) X✝).inv ≫ (colim ⋙ G).map f =
    ((whiskeringRight J C D).obj G ⋙ colim).map f ≫ ((fun F => preservesColimitIso G F) Y✝).inv
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ∀ (j : J),
    colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫
        ((fun F => preservesColimitIso G F) X✝).inv ≫ (colim ⋙ G).map f =
      colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫
        ((whiskeringRight J C D).obj G ⋙ colim).map f ≫ ((fun F => preservesColimitIso G F) Y✝).inv
[PROOFSTEP]
intro j
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫
      ((fun F => preservesColimitIso G F) X✝).inv ≫ (colim ⋙ G).map f =
    colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫
      ((whiskeringRight J C D).obj G ⋙ colim).map f ≫ ((fun F => preservesColimitIso G F) Y✝).inv
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    colimit.ι (X✝ ⋙ G) j ≫ colimMap (whiskerRight f G) ≫ (preservesColimitIso G Y✝).inv
[PROOFSTEP]
erw [ι_colimMap_assoc]
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    NatTrans.app (whiskerRight f G) j ≫ colimit.ι (Y✝ ⋙ G) j ≫ (preservesColimitIso G Y✝).inv
[PROOFSTEP]
simp only [ι_preservesColimitsIso_inv, whiskerRight_app, Category.assoc, ι_preservesColimitsIso_inv_assoc, ← G.map_comp]
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ G.map (colimit.ι X✝ j ≫ colimMap f) = G.map (NatTrans.app f j ≫ colimit.ι Y✝ j)
[PROOFSTEP]
erw [ι_colimMap]
