∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {i j : 𝒰.I₀} (xi : ↥(𝒰.X i))
  (xj : ↥(𝒰.X j)), (𝒰.f i) xi = (𝒰.f j) xj → ∃ k fi fj xk, (𝒰.trans fi) xk = xi ∧ (𝒰.trans fj) xk = xj