-- 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)
w :
  Eq.{v₁ + 1} (α :=
    ((Grothendieck.ι F X).obj d).base ⟶ ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).base)
    (Grothendieck.Hom.base
      { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) })
    (Grothendieck.Hom.base
      (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) }))
⊢ 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 ⋯,
        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) })
have w₁ : Eq.{u_2 + 1} (α :=
  obj
      (Cat.Hom.toFunctor
        (F.map
          (Grothendieck.Hom.base
            (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) :
                  ((Grothendieck.ι F X).obj d).Hom ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)) }
                { base := g,
                  fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) :
                  ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).Hom
                    ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))) })
              { 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) :
                ((Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))).Hom
                  ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)) }))))
      ((Grothendieck.ι F X).obj d).fiber ⟶
    ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)).fiber)
  (CategoryStruct.comp (Y :=
    obj
      (Cat.Hom.toFunctor
        (F.map
          (Grothendieck.Hom.base
            { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) :
              ((Grothendieck.ι F X).obj d).Hom ((Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)) })))
      ((Grothendieck.ι F X).obj d).fiber)
    (eqToHom sorry)
    (Grothendieck.Hom.fiber
      { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) }))
  (Grothendieck.Hom.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: fapply Grothendieck.ext