Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: case e_a
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 =
    (((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))

Tactic:
apply limit.hom_ext

Goal state after:
case e_a
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₁)
⊢ ∀ (j : J),
    (((((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) ≫
        limit.π ((K ⋙ fiberwiseColim F H) ⋙ (evaluation C H).obj c₂) j =
      ((((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))) ≫
        limit.π ((K ⋙ fiberwiseColim F H) ⋙ (evaluation C H).obj c₂) j