∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {D : Type u_5}
  [inst_1 : CategoryTheory.Category.{u_4, u_5} D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G)
  ⦃X Y : AlgebraicGeometry.PresheafedSpace C⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (G.mapPresheaf.map f)
      { base := CategoryTheory.CategoryStruct.id ↑(G.mapPresheaf.obj Y),
        c :=
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerLeft Y.presheaf α)
            (CategoryTheory.eqToHom ⋯) } =
    CategoryTheory.CategoryStruct.comp
      { base := CategoryTheory.CategoryStruct.id ↑(G.mapPresheaf.obj X),
        c :=
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerLeft X.presheaf α)
            (CategoryTheory.eqToHom ⋯) }
      (F.mapPresheaf.map f)