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₂
d : ↑(F.obj c₁)
⊢ colimit.ι (Grothendieck.ι F c₁ ⋙ limit K) d ≫
      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) d ≫
      (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:
simp only [← Category.assoc]

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₂
d : ↑(F.obj c₁)
⊢ (((((colimit.ι (Grothendieck.ι F c₁ ⋙ limit K) d ≫
                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) d ≫
              (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