-- 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
⊢ { 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 := 𝟙 { 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 }
have apply : Eq (α :=
  obj
      (Cat.Hom.toFunctor
        (F.map
          (Hom.base
            ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom sorry ≫ f :
                { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
              { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom sorry ≫ 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 sorry ≫ f ≫ g :
                  { base := c, fiber := X : Grothendieck F }.Hom
                    { base := c, fiber := Z : Grothendieck F } }.base).toFunctor.obj
        { base := c, fiber := X }.fiber)
      (eqToHom sorry) { base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom sorry ≫ f ≫ g }.fiber :
    obj
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom sorry ≫ f :
                  { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
                { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom sorry ≫ 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 sorry ≫ f :
          { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
        { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom sorry ≫ g }) :
    obj
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              ({ base := 𝟙 { base := c, fiber := X : Grothendieck F }.base, fiber := eqToHom sorry ≫ f :
                  { base := c, fiber := X : Grothendieck F }.Hom { base := c, fiber := Y : Grothendieck F } } ≫
                { base := 𝟙 { base := c, fiber := Y : Grothendieck F }.base, fiber := eqToHom sorry ≫ 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)
Tactic: apply Grothendieck.ext _ _ (by simp)