awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
R : CommRingCat
f : (↑R : Type u)
hf :
  IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
          (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base
            (InducedCategory.Hom.hom
              (LocallyRingedSpace.Hom.toShHom
                (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
      (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
x : ↥(Spec (CommRingCat.of (Localization.Away f)))
⊢ IsIso (X :=
    (Spec (CommRingCat.of (↑R : Type u))).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
            (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom
                (LocallyRingedSpace.Hom.toShHom
                  (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))))) :
          (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
        x))
    (PresheafedSpace.Hom.stalkMap
      (InducedCategory.Hom.hom
        (LocallyRingedSpace.Hom.toShHom
          (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))))
      x)

Tactic:
isIso_SpecMap_stakMap_localization R (Submonoid.powers f) x

Premises used: Set.Mem, Quiver.Hom.unop, Submonoid.powers, AlgebraicGeometry.isIso_SpecMap_stakMap_localization
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
R : CommRingCat
f : (↑R : Type u)
hf :
  IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
          (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base
            (InducedCategory.Hom.hom
              (LocallyRingedSpace.Hom.toShHom
                (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
      (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
x : ↥(Spec (CommRingCat.of (Localization.Away f)))
⊢ IsIso (X :=
    (Spec (CommRingCat.of (↑R : Type u))).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
            (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom
                (LocallyRingedSpace.Hom.toShHom
                  (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))))) :
          (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
        x))
    (PresheafedSpace.Hom.stalkMap
      (InducedCategory.Hom.hom
        (LocallyRingedSpace.Hom.toShHom
          (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))))
      x)

Tactic:
exact isIso_SpecMap_stakMap_localization R (Submonoid.powers f) x

Premises used: Submonoid.powers, AlgebraicGeometry.isIso_SpecMap_stakMap_localization
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
R : Type u_1
inst_1 : CommRing R
f : R
⊢ IsOpenImmersion (X := Spec (CommRingCat.of (Localization.Away f))) (Y := Spec (CommRingCat.of R))
    (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f))))

Tactic:
isOpenImmersion_SpecMap_localizationAway (R := .of R) f

Premises used: Set.Mem, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
⊢ Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)

Tactic:
have e := (IsLocalization.algEquiv (.powers f) S
    (Localization.Away f)).symm.toAlgHom.comp_algebraMap
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
rw :
  IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map
        (CommRingCat.ofHom
          (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
                Localization.Away f →ₐ[R] S) :
            Localization.Away f →+* S)))
      (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))))
⊢ IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (Spec.map (CommRingCat.ofHom (algebraMap R S)))

Tactic:
rw [← e, CommRingCat.ofHom_comp, Spec.map_comp]

Premises used: AlgebraicGeometry.Spec.map_comp, CommRingCat.ofHom_comp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
⊢ IsIso (X := CommRingCat.of (Localization.Away f)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
          Localization.Away f →ₐ[R] S)))

Tactic:
inferInstanceAs (IsIso <| (IsLocalization.algEquiv
      (Submonoid.powers f) S (Localization.Away f)).toRingEquiv.toCommRingCatIso.inv)

Premises used: _private.0.AlgebraicGeometry.IsOpenImmersion.of_isLocalization._proof_1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
⊢ IsIso (X := CommRingCat.of (Localization.Away f)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
          Localization.Away f →ₐ[R] S)))

Tactic:
exact inferInstanceAs (IsIso <| (IsLocalization.algEquiv
      (Submonoid.powers f) S (Localization.Away f)).toRingEquiv.toCommRingCatIso.inv)
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
⊢ IsIso (X := CommRingCat.of (Localization.Away f)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
          Localization.Away f →ₐ[R] S)))

Tactic:
have H : IsIso (CommRingCat.ofHom (IsLocalization.algEquiv
    (Submonoid.powers f) S (Localization.Away f)).symm.toAlgHom.toRingHom) := by
    exact inferInstanceAs (IsIso <| (IsLocalization.algEquiv
      (Submonoid.powers f) S (Localization.Away f)).toRingEquiv.toCommRingCatIso.inv)
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
H :
  IsIso (X := CommRingCat.of (Localization.Away f)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
          Localization.Away f →ₐ[R] S)))
simp :
  IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map
        (CommRingCat.ofHom
          (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →+* S)))
      (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))))
⊢ IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map
        (CommRingCat.ofHom
          (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
                Localization.Away f →ₐ[R] S) :
            Localization.Away f →+* S)))
      (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))))

Tactic:
simp only [AlgHom.toRingHom_eq_coe, AlgEquiv.toAlgHom_toRingHom] at H ⊢

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f : R
inst_3 : IsLocalization.Away f S
e :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →ₐ[R] S) :
        Localization.Away f →+* S)
      (algebraMap R (Localization.Away f)))
    (algebraMap R S)
H :
  IsIso (X := CommRingCat.of (Localization.Away f)) (Y := CommRingCat.of S)
    (CommRingCat.ofHom
      (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
        Localization.Away f →+* S))
⊢ IsOpenImmersion (X := Spec (CommRingCat.of S)) (Y := Spec (CommRingCat.of R))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map
        (CommRingCat.ofHom
          (↑(AlgEquiv.symm (IsLocalization.algEquiv (Submonoid.powers f) S (Localization.Away f))) :
            Localization.Away f →+* S)))
      (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away f)))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
obtain :
  ∀ (V : TopologicalSpace.Opens (↑X.toTopCat : Type u)) (hxV : x ∈ V) (R : CommRingCat.{u})
    (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)),
    ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
      IsOpenImmersion f ∧
        Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)

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

Premises used: AlgebraicGeometry.Scheme.local_affine
-- 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)
⊢ 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))

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
-- 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))
obtain :
  ∀ (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))),
    ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
      IsOpenImmersion f ∧
        Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)

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

Premises used: TopologicalSpace.Opens.is_open', PrimeSpectrum.isBasis_basic_opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 ⋯ }
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)

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

Premises used: Localization.Away, inferInstance, And.intro, CommRingCat.of, Exists.intro
-- 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 ⋯ }
refine :
  Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away r)))) ⇑f) x ∧
    Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away r)))) ⇑f ⊆ (↑U : Set ↥X)
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X),
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)

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