∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{u_3, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] ⦃X_1 Y : 𝒰.I₀⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp (𝒰.functorOfLocallyDirected.map f) (𝒰.f Y) =
    CategoryTheory.CategoryStruct.comp (𝒰.f X_1) (((CategoryTheory.Functor.const 𝒰.I₀).obj X).map f)