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