-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens (↑X.toTopCat : Type u)
hxV : x ∈ V
R : CommRingCat
e :
  X.restrict (U :=
      Functor.obj (Opens.toTopCat X.toTopCat)
        (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
          TopologicalSpace.Opens (↑X.toTopCat : Type u)))
      ⋯ ≅
    Spec.toLocallyRingedSpace.obj (op R)
this :
  Membership.mem (α := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
    ((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            e.hom.base :
          (a : (↑(↑(X.restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
        (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
          x_1 ∈
            (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
              TopologicalSpace.Opens (↑X.toTopCat : Type u)))
          x hxV) :
      (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
r : (↑R : Type u)
hr :
  Membership.mem (α := PrimeSpectrum (↑(unop (op R)) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(unop (op R)) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            e.hom.base :
          (a : (↑(↑(X.restrict ⋯).toPresheafedSpace : TopCat) : Type u)) →
            (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
        (Subtype.mk (p := fun (x_1 : (↑X.toTopCat : Type u)) ↦
          x_1 ∈
            (↑(Subtype.mk (p := fun (U : TopologicalSpace.Opens (↑X.toTopCat : Type u)) ↦ x ∈ U) V hxV) :
              TopologicalSpace.Opens (↑X.toTopCat : Type u)))
          x hxV) :
      (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
hr' :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑(unop (op R)) : Type u))) ⊆
    (↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U) :
      Set (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  CategoryStruct.comp (Y := Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))))
    { toLRSHom' := e.inv ≫ X.ofRestrict ⋯ }
⊢ Membership.mem (γ := Set ↥X)
      (⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑R : Type u))))
      x ∧
    ⇑{ toLRSHom' := e.inv ≫ X.ofRestrict ⋯ } '' (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑R : Type u))) ⊆
      (↑U : Set ↥X)

Tactic:
⟨⟨_, hr, congr(($(e.hom_inv_id).base ⟨x, hxV⟩).1)⟩, Set.image_subset_iff.mpr hr'⟩

Premises used: Iff.mpr, congrArg, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Iso.hom_inv_id, id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, Subtype.mk, And.intro, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.image_subset_iff, Subtype.val, DFunLike.coe