-- 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
h :
  Eq (α := colimit (limit K) ⟶ colimit (K.obj j)) (colimMap (limit.π K j) : colimit (limit K) ⟶ colimit (K.obj j))
    (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))
⊢ CategoryStruct.comp (Y := limit (K ⋙ colim)) (limit.post K colim) (limit.π (K ⋙ colim) j) =
    i₂.hom ≫ limit.π (K ⋙ colim) j

Tactic:
simp only [colim_obj, Functor.comp_obj, limit.post_π, colim_map, Iso.trans_def,
      Iso.trans_assoc, Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π,
      fiberwiseColim_obj, isoWhiskerLeft_hom, NatTrans.comp_app, Functor.associator_hom_app,
      whiskerLeft_app, fiberwiseColimCompColimIso_hom_app, Category.id_comp,
      preservesLimitIso_hom_π_assoc, i₂]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Limits.fiberwiseColim_obj, CategoryTheory.Limits.limit.post_π, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Limits.colim_map, CategoryTheory.Iso.trans_assoc, CategoryTheory.Iso.trans_def, CategoryTheory.Limits.colim_obj, CategoryTheory.preservesLimitIso_hom_π_assoc, CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.fiberwiseColimCompColimIso_hom_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π, CategoryTheory.Functor.isoWhiskerLeft_hom, CategoryTheory.Category.id_comp