-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Grothendieck (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst_1 : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst_2 : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : (↑(F.obj X) : Type u_1)
⊢ Eq (α := G.obj ((Grothendieck.ι F X).obj d) ⟶ colimit (Grothendieck.ι F Z ⋙ G))
    (CategoryStruct.comp (Y := G.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)))
      (G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
    (CategoryStruct.comp (Y := (Grothendieck.ι F Z ⋙ G).obj ((F.map (f ≫ g)).toFunctor.obj d))
      (G.map
        (CategoryStruct.comp (Y := (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
          (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
            { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
            { base := g,
              fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) })
          { base := eqToHom ⋯,
            fiber :=
              (eqToHom ⋯ :
                obj
                    (Cat.Hom.toFunctor (F.map (eqToHom ⋯)) :
                      Functor.{u_2, u_2, u_1, u_1}
                        (↑(F.obj
                              ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).base) :
                          Type u_1)
                        (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base) : Type u_1))
                    ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).fiber ⟶
                  ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).fiber) }))
      (colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)))
have w : Eq (α := (Grothendieck.ι F X).obj d ⟶ (Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d))
  { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
  (CategoryStruct.comp (Y := (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
    (CategoryStruct.comp (Y := (Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d))
      { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }
      { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) })
    { base := eqToHom sorry,
      fiber :=
        (eqToHom sorry :
          obj
              (Cat.Hom.toFunctor (F.map (eqToHom sorry)) :
                Functor.{u_2, u_2, u_1, u_1}
                  (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).base) :
                    Type u_1)
                  (↑(F.obj ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base) : Type u_1))
              ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).fiber ⟶
            ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).fiber) })
Tactic: congr 2