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