-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem exists_affine_mem_range_and_range_subset
    {X : Scheme.{u}} {x : X} {U : X.Opens} (hxU : x ∈ U) :
    ∃ (R : CommRingCat) (f : Spec R ⟶ X),
      IsOpenImmersion f ∧ x ∈ Set.range f.base ∧ Set.range f.base ⊆ U

Proof state:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ ⇑(ConcreteCategory.hom { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }.base) '' ↑(PrimeSpectrum.basicOpen r) ∧
    ⇑(ConcreteCategory.hom { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }.base) '' ↑(PrimeSpectrum.basicOpen r) ⊆ ↑U

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

Result:
no goals

Proof state:
case intro.mk.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
⊢ ∃ R f,
    IsOpenImmersion f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑U

Tactic:
obtain ⟨_, ⟨_, ⟨r : R, rfl⟩, rfl⟩, hr, hr'⟩ :=
  PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open this (Opens.is_open' _)

Result:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
⊢ ∃ R f,
    IsOpenImmersion f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑U

Proof state:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑U

Tactic:
rw [Scheme.comp_base, TopCat.coe_comp, Set.range_comp]

Result:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      ⇑(ConcreteCategory.hom { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }.base) ''
        Set.range ⇑(ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))).base) ∧
    ⇑(ConcreteCategory.hom { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }.base) ''
        Set.range ⇑(ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))).base) ⊆
      ↑U

Proof state:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈
      ⇑(ConcreteCategory.hom { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }.base) ''
        Set.range ⇑(ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))).base) ∧
    ⇑(ConcreteCategory.hom { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }.base) ''
        Set.range ⇑(ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r)))).base) ⊆
      ↑U

Tactic:
erw [PrimeSpectrum.localization_away_comap_range (Localization.Away r) r]

Result:
case intro.mk.intro.intro.intro.intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : X.Opens
hxU : x ∈ U
V : TopologicalSpace.Opens ↑X.toTopCat
hxV : x ∈ V
R : CommRingCat
e : X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)
this : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U
r : ↑R
hr : (ConcreteCategory.hom e.hom.base) ⟨x, hxV⟩ ∈ ↑(PrimeSpectrum.basicOpen r)
hr' : ↑(PrimeSpectrum.basicOpen r) ⊆ ↑((Opens.map (e.inv.base ≫ V.inclusion')).obj U)
f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away r))) ≫ { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }
⊢ x ∈ ⇑(ConcreteCategory.hom { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }.base) '' ↑(PrimeSpectrum.basicOpen r) ∧
    ⇑(ConcreteCategory.hom { toHom_1 := e.inv ≫ X.ofRestrict ⋯ }.base) '' ↑(PrimeSpectrum.basicOpen r) ⊆ ↑U