-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)
refine_1 :
  ∀
    (hrx :
      Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₁ :
  ∀
    (hrx :
      Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (γ :=
        TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₂ :
  ∀
    (hrx :
      Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (IsAffineOpen.fromSpec hV ⁻¹ᵁ X.basicOpen r)
        ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₃ :
  ∀
    (hrx :
      Membership.mem (α := ↥X) (X.basicOpen r)
        ((IsAffineOpen.fromSpec hV)
            ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))) :
          ↥X))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₄ :
  ∀
    (hrx :
      Membership.mem (α := ↥X) (X.basicOpen r)
        (((IsAffineOpen.isoSpec hV).hom ≫ IsAffineOpen.fromSpec hV) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) :
          ↥X))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₅ :
  ∀
    (hrx :
      Membership.mem (α := ↥X) (X.basicOpen r)
        ((Scheme.Opens.toSpecΓ V ≫ IsAffineOpen.fromSpec hV) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₆ refine_1₇ refine_1₈ refine_1₉ :
  ∀
    (hrx :
      Membership.mem (α := ↥X) (X.basicOpen r) ((Scheme.Opens.ι V) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
⊢ x ∈ X.basicOpen r

Tactic:
rwa [← PrimeSpectrum.mem_basicOpen, IsAffineOpen.primeIdealOf,
      ← hV.fromSpec_preimage_basicOpen, Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply,
      IsAffineOpen.isoSpec_hom, IsAffineOpen.toSpecΓ_fromSpec] at hrx

Premises used: AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.IsAffineOpen.primeIdealOf, PrimeSpectrum.mem_basicOpen, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, AlgebraicGeometry.IsAffineOpen.toSpecΓ_fromSpec