Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁴ : Category.{v₂, u₂} H
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
F : C ⥤ Cat
K : J ⥤ Grothendieck F ⥤ H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : HasLimitsOfShape J H
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ colimMap
        (whiskerRight (Grothendieck.ιNatTrans f) (limit K) ≫
          ((F.map f).toFunctor.associator (Grothendieck.ι F c₂) (limit K)).hom) ≫
      colimit.pre (Grothendieck.ι F c₂ ⋙ limit K) (F.map f).toFunctor ≫
        (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₂)).symm).hom ≫
          (preservesLimitIso colim
                (K ⋙ (whiskeringLeft (↑(F.obj c₂)) (Grothendieck F) H).obj (Grothendieck.ι F c₂))).hom ≫
            (HasLimit.isoOfNatIso
                  (K.associator ((whiskeringLeft (↑(F.obj c₂)) (Grothendieck F) H).obj (Grothendieck.ι F c₂)) colim ≪≫
                    K.isoWhiskerLeft (fiberwiseColimCompEvaluationIso c₂).symm ≪≫
                      (K.associator (fiberwiseColim F H) ((evaluation C H).obj c₂)).symm)).hom ≫
              (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₂).inv =
    (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₁)).symm).hom ≫
      (preservesLimitIso colim (K ⋙ (whiskeringLeft (↑(F.obj c₁)) (Grothendieck F) H).obj (Grothendieck.ι F c₁))).hom ≫
        (HasLimit.isoOfNatIso
              (K.associator ((whiskeringLeft (↑(F.obj c₁)) (Grothendieck F) H).obj (Grothendieck.ι F c₁)) colim ≪≫
                K.isoWhiskerLeft (fiberwiseColimCompEvaluationIso c₁).symm ≪≫
                  (K.associator (fiberwiseColim F H) ((evaluation C H).obj c₁)).symm)).hom ≫
          limMap ((K ⋙ fiberwiseColim F H).whiskerLeft ((evaluation C H).map f)) ≫
            (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₂).inv

Tactic:
apply colimit.hom_ext

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
H : Type u₂
inst✝⁴ : Category.{v₂, u₂} H
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
F : C ⥤ Cat
K : J ⥤ Grothendieck F ⥤ H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : HasLimitsOfShape J H
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ ∀ (j : ↑(F.obj c₁)),
    colimit.ι (Grothendieck.ι F c₁ ⋙ limit K) j ≫
        colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) (limit K) ≫
              ((F.map f).toFunctor.associator (Grothendieck.ι F c₂) (limit K)).hom) ≫
          colimit.pre (Grothendieck.ι F c₂ ⋙ limit K) (F.map f).toFunctor ≫
            (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₂)).symm).hom ≫
              (preservesLimitIso colim
                    (K ⋙ (whiskeringLeft (↑(F.obj c₂)) (Grothendieck F) H).obj (Grothendieck.ι F c₂))).hom ≫
                (HasLimit.isoOfNatIso
                      (K.associator ((whiskeringLeft (↑(F.obj c₂)) (Grothendieck F) H).obj (Grothendieck.ι F c₂))
                          colim ≪≫
                        K.isoWhiskerLeft (fiberwiseColimCompEvaluationIso c₂).symm ≪≫
                          (K.associator (fiberwiseColim F H) ((evaluation C H).obj c₂)).symm)).hom ≫
                  (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₂).inv =
      colimit.ι (Grothendieck.ι F c₁ ⋙ limit K) j ≫
        (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₁)).symm).hom ≫
          (preservesLimitIso colim
                (K ⋙ (whiskeringLeft (↑(F.obj c₁)) (Grothendieck F) H).obj (Grothendieck.ι F c₁))).hom ≫
            (HasLimit.isoOfNatIso
                  (K.associator ((whiskeringLeft (↑(F.obj c₁)) (Grothendieck F) H).obj (Grothendieck.ι F c₁)) colim ≪≫
                    K.isoWhiskerLeft (fiberwiseColimCompEvaluationIso c₁).symm ≪≫
                      (K.associator (fiberwiseColim F H) ((evaluation C H).obj c₁)).symm)).hom ≫
              limMap ((K ⋙ fiberwiseColim F H).whiskerLeft ((evaluation C H).map f)) ≫
                (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₂).inv