∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (J : Type u_1)
  (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↥X), ∃ j y, (map j) y = x)
  (map_prop : autoParam (∀ (j : J), P (map j)) AlgebraicGeometry.Scheme.Cover.mkOfCovers._auto_1),
  (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).I₀ = J