∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover)
  [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)]
  [∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), AlgebraicGeometry.IsAffine ((𝒱 i).X j)],
  AlgebraicGeometry.IsClosedImmersion
    (CategoryTheory.Limits.pullback.diagonal f ∣_ AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱)