-- 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 G : C ⥤ Cat
α : F ⟶ G
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ { base := (f ≫ g).base,
      fiber :=
        (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Z.base)) (f ≫ g).fiber :
      { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
        { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } } =
    { base := f.base,
        fiber :=
          (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
        { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
          { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
      { base := g.base,
        fiber :=
          (Cat.Hom₂.toNatTrans (eqToHom ⋯)).app Y.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber }
have apply : Eq (α :=
  obj
      (Cat.Hom.toFunctor
        (G.map
          (Hom.base
            ({ base := f.base,
                fiber :=
                  (Cat.Hom₂.toNatTrans (eqToHom sorry)).app X.fiber ≫
                    Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                  { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
              { base := g.base,
                fiber :=
                  (Cat.Hom₂.toNatTrans (eqToHom sorry)).app Y.fiber ≫
                    Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                  { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
      { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.fiber ⟶
    { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G }.fiber)
  (CategoryStruct.comp (Y :=
      (G.map
              { base := (f ≫ g).base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom sorry)).app X.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Z.base)) (f ≫ g).fiber :
                  { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                    { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber :
                      Grothendieck G } }.base).toFunctor.obj
        { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber }.fiber)
      (eqToHom sorry)
      { base := (f ≫ g).base,
          fiber :=
            (Cat.Hom₂.toNatTrans (eqToHom sorry)).app X.fiber ≫
              Functor.map (Cat.Hom.toFunctor (α.app Z.base)) (f ≫ g).fiber }.fiber :
    obj
        (Cat.Hom.toFunctor
          (G.map
            (Hom.base
              ({ base := f.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom sorry)).app X.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                  { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                    { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
                { base := g.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom sorry)).app Y.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                  { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                    { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
        { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.fiber ⟶
      { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G }.fiber)
  (Hom.fiber
      ({ base := f.base,
          fiber :=
            (Cat.Hom₂.toNatTrans (eqToHom sorry)).app X.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
          { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
            { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
        { base := g.base,
          fiber :=
            (Cat.Hom₂.toNatTrans (eqToHom sorry)).app Y.fiber ≫ Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber }) :
    obj
        (Cat.Hom.toFunctor
          (G.map
            (Hom.base
              ({ base := f.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom sorry)).app X.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Y.base)) f.fiber :
                  { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.Hom
                    { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G } } ≫
                { base := g.base,
                  fiber :=
                    (Cat.Hom₂.toNatTrans (eqToHom sorry)).app Y.fiber ≫
                      Functor.map (Cat.Hom.toFunctor (α.app Z.base)) g.fiber :
                  { base := Y.base, fiber := obj (Cat.Hom.toFunctor (α.app Y.base)) Y.fiber : Grothendieck G }.Hom
                    { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G } }))))
        { base := X.base, fiber := obj (Cat.Hom.toFunctor (α.app X.base)) X.fiber : Grothendieck G }.fiber ⟶
      { base := Z.base, fiber := obj (Cat.Hom.toFunctor (α.app Z.base)) Z.fiber : Grothendieck G }.fiber)
Tactic: apply Grothendieck.ext _ _ (by simp)