∀ {σ : Type u_2} {A : Type u_1} [inst : CommRing A] [inst_1 : SetLike σ A] (𝒜 : ℕ → σ) {X : AlgebraicGeometry.Scheme}
  (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) {x x' : ↑(X.presheaf.obj (Opposite.op ⊤))} {t t' : A} {d d' : ℕ}
  {H : f t = x} {H' : f t' = x'} {h0d' : 0 < d'} {hd' : t' ∈ 𝒜 d'} {s : A},
  t * s = t' → ∀ {n : ℕ}, d + n = d' → X.basicOpen x' ≤ X.basicOpen x