-- 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 ⋯ }
⊢ ∃ R f,
    IsOpenImmersion f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑U

Tactic:
refine ⟨.of (Localization.Away r), f, inferInstance, ?_⟩

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 ∈ 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)
⊢ ∃ R f,
    IsOpenImmersion f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑U

Tactic:
let f : Spec (CommRingCat.of (Localization.Away r)) ⟶ X :=
  Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away r))) ≫ ⟨e.inv ≫ X.ofRestrict _⟩

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 ⋯ }
⊢ ∃ 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
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)
⊢ ∃ R f,
    IsOpenImmersion f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑U

Tactic:
have : e.hom.base ⟨x, hxV⟩ ∈ (Opens.map (e.inv.base ≫ V.inclusion')).obj U :=
  show ((e.hom ≫ e.inv).base ⟨x, hxV⟩).1 ∈ U from e.hom_inv_id ▸ hxU

Result:
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

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
U : X.Opens
hxU : x ∈ U
⊢ ∃ R f,
    IsOpenImmersion f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑U

Tactic:
obtain ⟨⟨V, hxV⟩, R, ⟨e⟩⟩ := X.2 x

Result:
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)
⊢ ∃ R f,
    IsOpenImmersion f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑U