Module: Mathlib.CategoryTheory.Limits.Preserves.Grothendieck

Goal state before:
pp: case e'_5
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
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans
    (Trans.trans
      (Trans.trans (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm)
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
e_3✝ : colim.obj (limit K) = colimit (limit K)
j✝¹ : J
j✝ : Grothendieck F
⊢ colimit.ι (limit K) j✝ ≫ colimMap (limit.π K j✝¹) =
    colimit.ι (limit K) j✝ ≫
      (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm).hom ≫
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)).hom ≫
          colimMap (limit.π (K ⋙ fiberwiseColim F H) j✝¹) ≫ (colimitFiberwiseColimitIso (K.obj j✝¹)).hom

Tactic:
simp only [ι_colimMap, Trans.trans, Iso.symm_hom, ι_colimitFiberwiseColimitIso_inv_assoc,
      HasColimit.isoOfNatIso_ι_hom_assoc, fiberwiseColimit_obj, fiberwiseColimitLimitIso_hom_app,
      ι_colimMap_assoc, Category.assoc, limitObjIsoLimitCompEvaluation_inv_π_app_assoc,
      Functor.comp_obj, fiberwiseColim_obj, HasLimit.isoOfNatIso_hom_π_assoc,
      whiskeringLeft_obj_obj, colim_obj, evaluation_obj_obj, Iso.trans_hom, isoWhiskerLeft_hom,
      NatTrans.comp_app, Functor.associator_hom_app, whiskerLeft_app,
      fiberwiseColimCompEvaluationIso_inv_app, Functor.associator_inv_app, Category.comp_id,
      Category.id_comp, preservesLimitIso_hom_π_assoc, colim_map, Grothendieck.ι_obj,
      ι_colimitFiberwiseColimitIso_hom]

Goal state after:
case e'_5
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
inst✝⁴ : HasColimitsOfShape C H
inst✝³ : HasLimitsOfShape J H
inst✝² : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
inst✝¹ : PreservesLimitsOfShape J colim
inst✝ : ∀ (c : C), PreservesLimitsOfShape J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans
    (Trans.trans
      (Trans.trans (Trans.trans ⋯ (colimitFiberwiseColimitIso (limit K)).symm)
        (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
e_3✝ : colim.obj (limit K) = colimit (limit K)
j✝¹ : J
j✝ : Grothendieck F
⊢ (limit.π K j✝¹).app j✝ ≫ colimit.ι (K.obj j✝¹) j✝ =
    (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F j✝.base)).inv.app j✝.fiber ≫
      (limit.π (K ⋙ (whiskeringLeft (↑(F.obj j✝.base)) (Grothendieck F) H).obj (Grothendieck.ι F j✝.base)) j✝¹).app
          j✝.fiber ≫
        colimit.ι (K.obj j✝¹) { base := j✝.base, fiber := j✝.fiber }