-- Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
H : Type u₂
inst_1 : Category.{v₂, u₂} H
J : Type u₃
inst_2 : Category.{v₃, u₃} J
F : C ⥤ Cat
K : J ⥤ Grothendieck F ⥤ H
inst_3 : ∀ (c : C), HasColimitsOfShape.{v₄, u₄, v₂, u₂} (↑(F.obj c) : Type u₄) H
inst_4 : HasLimitsOfShape.{v₃, u₃, v₂, u₂} J H
inst_5 : ∀ (c : C), PreservesLimitsOfShape (C := Functor.{v₄, v₂, u₄, u₂} (↑(F.obj c) : Type u₄) H) J colim
c₁ c₂ : C
f : c₁ ⟶ c₂
simp :
  Eq (α := colimit (Grothendieck.ι F c₁ ⋙ limit K) ⟶ (limit (K ⋙ fiberwiseColim F H)).obj c₂)
    (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F c₂ ⋙ limit K))
        (colimMap
          (whiskerRight (Grothendieck.ιNatTrans f) (limit K) ≫
            ((F.map f).toFunctor.associator (Grothendieck.ι F c₂) (limit K)).hom))
        (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₂ ⋙ limit K))
          (colimit.pre (Grothendieck.ι F c₂ ⋙ limit K) (F.map f).toFunctor)
          (CategoryStruct.comp (Y :=
            colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))))
            (Iso.hom (HasColimit.isoOfNatIso (Iso.symm (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₂)))) :
              colimit (Grothendieck.ι F c₂ ⋙ limit K) ⟶
                colimit
                  (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))))
            (CategoryStruct.comp (Y :=
                limit
                  ((K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂)) ⋙ colim))
                (Iso.hom
                  (preservesLimitIso colim
                    (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))))
                (CategoryStruct.comp (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂))
                  (Iso.hom
                      (HasLimit.isoOfNatIso
                        (K.associator
                            (obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))
                            colim ≪≫
                          K.isoWhiskerLeft (Iso.symm (fiberwiseColimCompEvaluationIso c₂)) ≪≫
                            (K.associator (fiberwiseColim F H) (obj (evaluation C H) c₂)).symm)) :
                    limit
                        ((K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂)) ⋙
                          colim) ⟶
                      limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂))
                  (Iso.inv (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₂) :
                    limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂) ⟶
                      (limit (K ⋙ fiberwiseColim F H)).obj c₂)) :
              colimit
                  (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))) ⟶
                (limit (K ⋙ fiberwiseColim F H)).obj c₂))) :
      colimit (Grothendieck.ι F c₁ ⋙ limit K) ⟶ (limit (K ⋙ fiberwiseColim F H)).obj c₂)
    (CategoryStruct.comp (Y :=
        colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))))
        (Iso.hom (HasColimit.isoOfNatIso (Iso.symm (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₁)))) :
          colimit (Grothendieck.ι F c₁ ⋙ limit K) ⟶
            colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))))
        (CategoryStruct.comp (Y :=
            limit ((K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁)) ⋙ colim))
            (Iso.hom
              (preservesLimitIso colim
                (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))))
            (CategoryStruct.comp (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₁))
              (Iso.hom
                (HasLimit.isoOfNatIso
                  (K.associator (obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))
                      colim ≪≫
                    K.isoWhiskerLeft (Iso.symm (fiberwiseColimCompEvaluationIso c₁)) ≪≫
                      (K.associator (fiberwiseColim F H) (obj (evaluation C H) c₁)).symm)))
              (CategoryStruct.comp (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂))
                (limMap ((K ⋙ fiberwiseColim F H).whiskerLeft (map (evaluation C H) f)) :
                  limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₁) ⟶
                    limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂))
                (Iso.inv (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₂) :
                  limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂) ⟶
                    (limit (K ⋙ fiberwiseColim F H)).obj c₂))) :
          colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))) ⟶
            (limit (K ⋙ fiberwiseColim F H)).obj c₂) :
      colimit (Grothendieck.ι F c₁ ⋙ limit K) ⟶ (limit (K ⋙ fiberwiseColim F H)).obj c₂)
⊢ (fiberwiseColimit (limit K)).map f ≫
      Iso.hom
        ((fun (c : C) ↦
            (Iso.trans (Y :=
                colimit
                  (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c))))
                (HasColimit.isoOfNatIso (Iso.symm (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c))) :
                  colimit (Grothendieck.ι F c ⋙ limit K) ≅
                    colimit
                      (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c))))
                (Iso.trans (Y :=
                    limit
                      ((K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c)) ⋙
                        colim))
                    (preservesLimitIso colim
                      (K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c)))
                    (Iso.trans (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c))
                      (HasLimit.isoOfNatIso
                          (K.associator
                              (obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c))
                              colim ≪≫
                            K.isoWhiskerLeft (Iso.symm (fiberwiseColimCompEvaluationIso c)) ≪≫
                              (K.associator (fiberwiseColim F H) (obj (evaluation C H) c)).symm) :
                        limit
                            ((K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c)) ⋙
                              colim) ≅
                          limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c))
                      (Iso.symm (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c) :
                        limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c) ≅
                          (limit (K ⋙ fiberwiseColim F H)).obj c)) :
                  colimit
                      (limit
                        (K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c))) ≅
                    (limit (K ⋙ fiberwiseColim F H)).obj c) :
              (fiberwiseColimit (limit K)).obj c ≅ (limit (K ⋙ fiberwiseColim F H)).obj c))
          c₂) =
    Iso.hom
        ((fun (c : C) ↦
            (Iso.trans (Y :=
                colimit
                  (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c))))
                (HasColimit.isoOfNatIso (Iso.symm (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c))) :
                  colimit (Grothendieck.ι F c ⋙ limit K) ≅
                    colimit
                      (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c))))
                (Iso.trans (Y :=
                    limit
                      ((K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c)) ⋙
                        colim))
                    (preservesLimitIso colim
                      (K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c)))
                    (Iso.trans (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c))
                      (HasLimit.isoOfNatIso
                          (K.associator
                              (obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c))
                              colim ≪≫
                            K.isoWhiskerLeft (Iso.symm (fiberwiseColimCompEvaluationIso c)) ≪≫
                              (K.associator (fiberwiseColim F H) (obj (evaluation C H) c)).symm) :
                        limit
                            ((K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c)) ⋙
                              colim) ≅
                          limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c))
                      (Iso.symm (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c) :
                        limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c) ≅
                          (limit (K ⋙ fiberwiseColim F H)).obj c)) :
                  colimit
                      (limit
                        (K ⋙ obj (whiskeringLeft (↑(F.obj c) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c))) ≅
                    (limit (K ⋙ fiberwiseColim F H)).obj c) :
              (fiberwiseColimit (limit K)).obj c ≅ (limit (K ⋙ fiberwiseColim F H)).obj c))
          c₁) ≫
      (limit (K ⋙ fiberwiseColim F H)).map f

Tactic:
simp only [fiberwiseColimit_obj, fiberwiseColimit_map, Iso.trans_hom, Iso.symm_hom,
        Category.assoc, limitObjIsoLimitCompEvaluation_inv_limit_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.fiberwiseColimit_map, CategoryTheory.Limits.fiberwiseColimit_obj, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_limit_map, CategoryTheory.Iso.trans_hom