-- 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.{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 ⋯,
                  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) :
                  ((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 ⋯)
      (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 ⋯,
          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} (α := (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
  (eqToHom sorry : (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
  (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map (f ≫ g)).toFunctor.obj d)) (eqToHom sorry)
      (CategoryStruct.comp (Y := (F.map (𝟙 Z)).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)))
        ((F.map (𝟙 Z)).toFunctor.map (eqToHom sorry)) (eqToHom sorry)) :
    (F.map ((f ≫ g) ≫ 𝟙 Z)).toFunctor.obj d ⟶ (F.map (f ≫ g)).toFunctor.obj d)
Tactic: simp only [Grothendieck.ι_obj, eqToHom_refl,
        Grothendieck.comp_base, Category.comp_id, Grothendieck.comp_fiber, Functor.map_id]