-- 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, max ?u.65311 ?u.65312, u, max (?u.65311 + 1) (?u.65312 + 1)} C Cat
H : Functor.{v, max ?u.65343 ?u.65344, u, max (?u.65343 + 1) (?u.65344 + 1)} C Cat
X Y Z : Grothendieck (F ⋙ Cat.asSmallFunctor)
x : X ⟶ Y
x_1 : Y ⟶ Z
w_fiber :
  Eq (α :=
    obj
        (Cat.Hom.toFunctor
          (F.map
            (Hom.base
              ({ base := x.base, fiber := Functor.map AsSmall.down x.fiber :
                  { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
                    { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F } } ≫
                { base := x_1.base, fiber := Functor.map AsSmall.down x_1.fiber :
                  { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F }.Hom
                    { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F } }))))
        { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.fiber ⟶
      { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F }.fiber)
    (CategoryStruct.comp (Y :=
        (F.map
                { base := (x ≫ x_1).base, fiber := Functor.map AsSmall.down (x ≫ x_1).fiber :
                    { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
                      { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F } }.base).toFunctor.obj
          { base := X.base, fiber := obj AsSmall.down X.fiber }.fiber)
        (eqToHom ⋯) { base := (x ≫ x_1).base, fiber := Functor.map AsSmall.down (x ≫ x_1).fiber }.fiber :
      obj
          (Cat.Hom.toFunctor
            (F.map
              (Hom.base
                ({ base := x.base, fiber := Functor.map AsSmall.down x.fiber :
                    { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
                      { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F } } ≫
                  { base := x_1.base, fiber := Functor.map AsSmall.down x_1.fiber :
                    { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F }.Hom
                      { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F } }))))
          { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.fiber ⟶
        { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F }.fiber)
    (Hom.fiber
        ({ base := x.base, fiber := Functor.map AsSmall.down x.fiber :
            { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
              { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F } } ≫
          { base := x_1.base, fiber := Functor.map AsSmall.down x_1.fiber }) :
      obj
          (Cat.Hom.toFunctor
            (F.map
              (Hom.base
                ({ base := x.base, fiber := Functor.map AsSmall.down x.fiber :
                    { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
                      { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F } } ≫
                  { base := x_1.base, fiber := Functor.map AsSmall.down x_1.fiber :
                    { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F }.Hom
                      { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F } }))))
          { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.fiber ⟶
        { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F }.fiber)
⊢ { base := (x ≫ x_1).base, fiber := Functor.map AsSmall.down (x ≫ x_1).fiber :
      { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
        { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F } } =
    { base := x.base, fiber := Functor.map AsSmall.down x.fiber :
        { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
          { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F } } ≫
      { base := x_1.base, fiber := Functor.map AsSmall.down x_1.fiber }
have w_base : { base := (x ≫ x_1).base, fiber := Functor.map AsSmall.down (x ≫ x_1).fiber :
      { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
        { base := Z.base, fiber := obj AsSmall.down Z.fiber : Grothendieck F } }.base =
  Hom.base
    ({ base := x.base, fiber := Functor.map AsSmall.down x.fiber :
        { base := X.base, fiber := obj AsSmall.down X.fiber : Grothendieck F }.Hom
          { base := Y.base, fiber := obj AsSmall.down Y.fiber : Grothendieck F } } ≫
      { base := x_1.base, fiber := Functor.map AsSmall.down x_1.fiber })
Tactic: apply Grothendieck.ext