-- 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 :
  ∀ (j_1 : Grothendieck F),
    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))
⊢ 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))

Tactic:
ext