-- Lean 4 proof step from Mathlib.CategoryTheory.Grothendieck (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
G : Functor.{v, w, u, w + 1} C (Type w)
E : Type u_1
inst_2 : Category.{v_1, u_1} E
c : C
X Y Z : (↑(F.obj c) : Type u₂)
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    obj
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
                  { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
                { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g :
                  { base := c, fiber := Y : Grothendieck F }.Hom { base := c, fiber := Z : Grothendieck F } }))))
        { base := c, fiber := X : Grothendieck F }.fiber ⟶
      { base := c, fiber := Z : Grothendieck F }.fiber)
    (CategoryStruct.comp (Y :=
        (F.map
                { base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f ≫ g :
                    { base := c, fiber := X : Grothendieck F }.Hom
                      { base := c, fiber := Z : Grothendieck F } }.base).toFunctor.obj
          { base := c, fiber := X }.fiber)
        (eqToHom ⋯) { base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f ≫ g }.fiber :
      obj
          (Cat.Hom.toFunctor
            (F.map
              (Hom.base
                ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
                    { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
                  { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g :
                    { base := c, fiber := Y : Grothendieck F }.Hom { base := c, fiber := Z : Grothendieck F } }))))
          { base := c, fiber := X : Grothendieck F }.fiber ⟶
        { base := c, fiber := Z : Grothendieck F }.fiber)
    (Hom.fiber
        ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
            { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
          { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g }) :
      obj
          (Cat.Hom.toFunctor
            (F.map
              (Hom.base
                ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ f :
                    { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
                  { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom ⋯ ≫ g :
                    { base := c, fiber := Y : Grothendieck F }.Hom { base := c, fiber := Z : Grothendieck F } }))))
          { base := c, fiber := X : Grothendieck F }.fiber ⟶
        { base := c, fiber := Z : Grothendieck F }.fiber)
have simp : Eq (α := (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Z) ((eqToHom sorry ≫ f) ≫ g : (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Z)
  (CategoryStruct.comp (Y := (F.map (𝟙 c)).toFunctor.obj Y) (eqToHom sorry ≫ (F.map (𝟙 c)).toFunctor.map f) (eqToHom sorry) ≫
      g :
    (F.map (𝟙 c ≫ 𝟙 c)).toFunctor.obj X ⟶ Z)
Tactic: simp only [comp_base, ← Category.assoc, eqToHom_trans, comp_fiber, Functor.map_comp,
      eqToHom_map]