-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
s : (↑Γ(Y, U) : Type u_1)
hs :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U) :
          (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
inr :
  ∀ (V : TopologicalSpace.Opens ↥Y) (hV : V ∈ Y.affineOpens) (hxV : x ∈ (↑V : Set ↥Y)) (hVU : V ≤ U),
    ∃ (V : TopologicalSpace.Opens ↥Y) (hV : V ≤ Opposite.unop (Opposite.op U)),
      x ∈ V ∧
        Eq (α := (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
                (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                  (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
              s :
            (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
                (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                  (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
              0 :
            (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
⊢ ∃ (V : TopologicalSpace.Opens ↥Y) (hV : V ≤ Opposite.unop (Opposite.op U)),
    x ∈ V ∧
      Eq (α := (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            s :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hV).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            0 :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU : V ≤ U⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open hx U.isOpen

Premises used: TopologicalSpace.Opens.isOpen, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open