∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.RespectsIso] {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (J : Type u_2)
  (obj : J → AlgebraicGeometry.Scheme) (map : (i : J) → obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)),
  (∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) →
    { I₀ := J, X := obj, f := map }.presieve₀ ∈ (AlgebraicGeometry.Scheme.precoverage P).coverings X