-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Grothendieck (goal)
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
K : J ⥤ Grothendieck F ⥤ H
inst_3 : ∀ (c : C), HasColimitsOfShape.{v₄, u₄, v₂, u₂} (↑(F.obj c) : Type u₄) H
inst_4 : HasLimitsOfShape.{v₃, u₃, v₂, u₂} J H
inst_5 : ∀ (c : C), PreservesLimitsOfShape (C := Functor.{v₄, v₂, u₄, u₂} (↑(F.obj c) : Type u₄) H) J colim
c₁ c₂ : C
f : c₁ ⟶ c₂
d : (↑(F.obj c₁) : Type u₄)
⊢ Eq (α := (Grothendieck.ι F c₁ ⋙ limit K).obj d ⟶ limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂))
    (CategoryStruct.comp (Y :=
      limit ((K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂)) ⋙ colim))
      (CategoryStruct.comp (Y :=
        colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))))
        (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₂ ⋙ limit K))
            (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F c₂ ⋙ limit K))
              (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₁ ⋙ limit K))
                (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))
            (Iso.hom
              (HasColimit.isoOfNatIso (Iso.symm (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₂))))) :
          (Grothendieck.ι F c₁ ⋙ limit K).obj d ⟶
            colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))))
        (Iso.hom
            (preservesLimitIso colim
              (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))) :
          colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))) ⟶
            limit
              ((K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂)) ⋙ colim)))
      (Iso.hom
        (HasLimit.isoOfNatIso
          (K.associator (obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂)) colim ≪≫
            K.isoWhiskerLeft (Iso.symm (fiberwiseColimCompEvaluationIso c₂)) ≪≫
              (K.associator (fiberwiseColim F H) (obj (evaluation C H) c₂)).symm))))
    (CategoryStruct.comp (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₁))
      (CategoryStruct.comp (Y :=
        limit ((K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁)) ⋙ colim))
        (CategoryStruct.comp (Y :=
          colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))))
          (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₁ ⋙ limit K))
              (colimit.ι (Grothendieck.ι F c₁ ⋙ limit K) d)
              (Iso.hom
                (HasColimit.isoOfNatIso (Iso.symm (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₁))))) :
            (Grothendieck.ι F c₁ ⋙ limit K).obj d ⟶
              colimit
                (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))))
          (Iso.hom
              (preservesLimitIso colim
                (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))) :
            colimit
                (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))) ⟶
              limit
                ((K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁)) ⋙ colim)))
        (Iso.hom
          (HasLimit.isoOfNatIso
            (K.associator (obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))
                colim ≪≫
              K.isoWhiskerLeft (Iso.symm (fiberwiseColimCompEvaluationIso c₁)) ≪≫
                (K.associator (fiberwiseColim F H) (obj (evaluation C H) c₁)).symm))))
      (limMap ((K ⋙ fiberwiseColim F H).whiskerLeft (map (evaluation C H) f))))
have w : ∀ (j : J),
  CategoryStruct.comp (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂))
      (CategoryStruct.comp (Y :=
        limit ((K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂)) ⋙ colim))
        (CategoryStruct.comp (Y :=
          colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))))
          (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₂ ⋙ limit K))
              (CategoryStruct.comp (Y := colimit ((F.map f).toFunctor ⋙ Grothendieck.ι F c₂ ⋙ limit K))
                (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₁ ⋙ limit K))
                  (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))
              (Iso.hom
                (HasColimit.isoOfNatIso (Iso.symm (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₂))))) :
            (Grothendieck.ι F c₁ ⋙ limit K).obj d ⟶
              colimit
                (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))))
          (Iso.hom
              (preservesLimitIso colim
                (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))) :
            colimit
                (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))) ⟶
              limit
                ((K ⋙ obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂)) ⋙ colim)))
        (Iso.hom
          (HasLimit.isoOfNatIso
            (K.associator (obj (whiskeringLeft (↑(F.obj c₂) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₂))
                colim ≪≫
              K.isoWhiskerLeft (Iso.symm (fiberwiseColimCompEvaluationIso c₂)) ≪≫
                (K.associator (fiberwiseColim F H) (obj (evaluation C H) c₂)).symm))))
      (limit.π ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂) j) =
    CategoryStruct.comp (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂))
      (CategoryStruct.comp (Y := limit ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₁))
        (CategoryStruct.comp (Y :=
          limit ((K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁)) ⋙ colim))
          (CategoryStruct.comp (Y :=
            colimit (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))))
            (CategoryStruct.comp (Y := colimit (Grothendieck.ι F c₁ ⋙ limit K))
                (colimit.ι (Grothendieck.ι F c₁ ⋙ limit K) d)
                (Iso.hom
                  (HasColimit.isoOfNatIso (Iso.symm (limitCompWhiskeringLeftIsoCompLimit K (Grothendieck.ι F c₁))))) :
              (Grothendieck.ι F c₁ ⋙ limit K).obj d ⟶
                colimit
                  (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))))
            (Iso.hom
                (preservesLimitIso colim
                  (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))) :
              colimit
                  (limit (K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))) ⟶
                limit
                  ((K ⋙ obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁)) ⋙
                    colim)))
          (Iso.hom
            (HasLimit.isoOfNatIso
              (K.associator (obj (whiskeringLeft (↑(F.obj c₁) : Type u₄) (Grothendieck F) H) (Grothendieck.ι F c₁))
                  colim ≪≫
                K.isoWhiskerLeft (Iso.symm (fiberwiseColimCompEvaluationIso c₁)) ≪≫
                  (K.associator (fiberwiseColim F H) (obj (evaluation C H) c₁)).symm))))
        (limMap ((K ⋙ fiberwiseColim F H).whiskerLeft (map (evaluation C H) f))))
      (limit.π ((K ⋙ fiberwiseColim F H) ⋙ obj (evaluation C H) c₂) j)
Tactic: apply limit.hom_ext