-- 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
inst_3 : HasColimitsOfShape.{v₁, u₁, v₂, u₂} C H
inst_4 : HasLimitsOfShape.{v₃, u₃, v₂, u₂} J H
inst_5 : ∀ (c : C), HasColimitsOfShape.{v₄, u₄, v₂, u₂} (↑(F.obj c) : Type u₄) H
inst_6 : PreservesLimitsOfShape (C := Functor.{v₁, v₂, u₁, u₂} C H) J colim
inst_7 : ∀ (c : C), PreservesLimitsOfShape (C := Functor.{v₄, v₂, u₄, u₂} (↑(F.obj c) : Type u₄) H) J colim
K : J ⥤ Grothendieck F ⥤ H
i₂ : colimit (limit K) ≅ limit (K ⋙ colim) :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := limit ((K ⋙ fiberwiseColim F H) ⋙ colim))
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := colimit (limit (K ⋙ fiberwiseColim F H)))
      (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : H) ↦ x1 ≅ x2) (b := colimit (fiberwiseColimit (limit K)))
          (Trans.trans (r := Eq) (s := Iso) (t := Iso) ⋯ (Iso.symm (colimitFiberwiseColimitIso (limit K))) :
            colimit (limit K) ≅ colimit (fiberwiseColimit (limit K)))
          (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K) :
            colimit (fiberwiseColimit (limit K)) ≅ colimit (limit (K ⋙ fiberwiseColim F H))) :
        colimit (limit K) ≅ colimit (limit (K ⋙ fiberwiseColim F H)))
      (preservesLimitIso colim (K ⋙ fiberwiseColim F H) :
        obj colim (limit (K ⋙ fiberwiseColim F H)) ≅ limit ((K ⋙ fiberwiseColim F H) ⋙ colim)))
    (HasLimit.isoOfNatIso (K.associator (fiberwiseColim F H) colim ≪≫ K.isoWhiskerLeft fiberwiseColimCompColimIso))
e_3 : obj colim (limit K) = colimit (limit K)
j : J
j_1 : Grothendieck F
h :
  Eq (α := (limit K).obj j_1 ⟶ colimit (K.obj j)) (NatTrans.app (limit.π K j) j_1 ≫ colimit.ι (K.obj j) j_1)
    (CategoryStruct.comp (Y :=
      obj
        (limit (K ⋙ obj (whiskeringLeft (↑(F.obj j_1.base) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F j_1.base)))
        j_1.fiber)
      (NatTrans.app (Iso.inv (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F j_1.base))) j_1.fiber)
      (NatTrans.app
          (limit.π
            (K ⋙ obj (whiskeringLeft (↑(F.obj j_1.base) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F j_1.base)) j)
          j_1.fiber ≫
        colimit.ι (K.obj j) { base := j_1.base, fiber := j_1.fiber }))
⊢ Eq (α := (limit K).obj j_1 ⟶ colimit (K.obj j))
    (CategoryStruct.comp (Y := colimit (limit K)) (colimit.ι (limit K) j_1) (colimMap (limit.π K j)) :
      (limit K).obj j_1 ⟶ colimit (K.obj j))
    (CategoryStruct.comp (Y := colimit (limit K)) (colimit.ι (limit K) j_1 : (limit K).obj j_1 ⟶ colimit (limit K))
        (CategoryStruct.comp (Y := colimit (fiberwiseColimit (limit K)))
            (Iso.hom (Trans.trans (r := Eq) (s := Iso) (t := Iso) ⋯ (Iso.symm (colimitFiberwiseColimitIso (limit K)))) :
              colimit (limit K) ⟶ colimit (fiberwiseColimit (limit K)))
            (CategoryStruct.comp (Y := colimit (limit (K ⋙ fiberwiseColim F H)))
                (Iso.hom (HasColimit.isoOfNatIso (fiberwiseColimitLimitIso K)) :
                  colimit (fiberwiseColimit (limit K)) ⟶ colimit (limit (K ⋙ fiberwiseColim F H)))
                (CategoryStruct.comp (Y := colimit (fiberwiseColimit (K.obj j)))
                    (colimMap (limit.π (K ⋙ fiberwiseColim F H) j)) (Iso.hom (colimitFiberwiseColimitIso (K.obj j))) :
                  colimit (limit (K ⋙ fiberwiseColim F H)) ⟶ colimit (K.obj j)) :
              colimit (fiberwiseColimit (limit K)) ⟶ colimit (K.obj j)) :
          colimit (limit K) ⟶ colimit (K.obj j)) :
      (limit K).obj j_1 ⟶ colimit (K.obj j))

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]

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