∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ G) (X : CategoryTheory.Grothendieck F),
  { base := (CategoryTheory.CategoryStruct.id X).base,
      fiber :=
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.eqToHom ⋯).toNatTrans.app X.fiber)
          ((α.app X.base).toFunctor.map (CategoryTheory.CategoryStruct.id X).fiber) } =
    CategoryTheory.CategoryStruct.id { base := X.base, fiber := (α.app X.base).toFunctor.obj X.fiber }