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₂
⊢ (fiberwiseColimit (limit K)).map f ≫
      (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₂)).symm ≪≫
          preservesLimitIso colim (K ⋙ (whiskeringLeft (↑(F.obj c₂)) (Grothendieck F) H).obj (Grothendieck.ι F c₂)) ≪≫
            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) ≪≫
              (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₂).symm).hom =
    (HasColimit.isoOfNatIso (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₁)).symm ≪≫
          preservesLimitIso colim (K ⋙ (whiskeringLeft (↑(F.obj c₁)) (Grothendieck F) H).obj (Grothendieck.ι F c₁)) ≪≫
            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) ≪≫
              (limitObjIsoLimitCompEvaluation (K ⋙ fiberwiseColim F H) c₁).symm).hom ≫
      (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]

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₂
⊢ 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