awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
apply : IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) {hU.primeIdealOf x}
⊢ (hU.primeIdealOf x).asIdeal.IsMaximal

Tactic:
apply (hU.primeIdealOf x).isClosed_singleton_iff_isMaximal.mp

Premises used: PrimeSpectrum.isClosed_singleton_iff_isMaximal, Iff.mp, AlgebraicGeometry.IsAffineOpen.primeIdealOf
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
rw : IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) (Set.image (α := ↥U) ⇑hU.isoSpec.hom {x})
⊢ IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) {hU.primeIdealOf x}

Tactic:
rw [primeIdealOf, ← Set.image_singleton]

Premises used: Set.image_singleton, AlgebraicGeometry.IsAffineOpen.primeIdealOf
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
⊢ IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) (Set.image (α := ↥U) ⇑hU.isoSpec.hom {x})

Tactic:
(Topology.IsClosedEmbedding.isClosed_iff_image_isClosed <|
    IsHomeomorph.isClosedEmbedding ?_).mp hx₀

Premises used: IsHomeomorph.isClosedEmbedding, Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
refine : IsHomeomorph (X := ↥U) (Y := PrimeSpectrum (↑Γ(X, U) : Type u)) ⇑hU.isoSpec.hom
⊢ IsClosed (X := PrimeSpectrum (↑Γ(X, U) : Type u)) (Set.image (α := ↥U) ⇑hU.isoSpec.hom {x})

Tactic:
refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed <|
    IsHomeomorph.isClosedEmbedding ?_).mp hx₀

Premises used: IsHomeomorph.isClosedEmbedding, Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
apply : IsIso hU.isoSpec.hom.base
⊢ IsHomeomorph (X := ↥U) (Y := PrimeSpectrum (↑Γ(X, U) : Type u)) ⇑hU.isoSpec.hom

Tactic:
apply (TopCat.isIso_iff_isHomeomorph _).mp

Premises used: TopCat.isIso_iff_isHomeomorph, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
hx₀ : IsClosed (X := ↥U) {x}
⊢ IsIso hU.isoSpec.hom.base

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
_ : IsLocalization y.asIdeal.primeCompl (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec y)) : Type u) y.asIdeal

Tactic:
apply
    (@IsLocalization.isLocalization_iff_of_ringEquiv (R := Γ(X, U))
      (S := X.presheaf.stalk (hU.fromSpec y)) _ y.asIdeal.primeCompl _
      (TopCat.Presheaf.algebra_section_stalk X.presheaf ⟨hU.fromSpec y, hy⟩) _ _
      (asIso <| hU.fromSpec.stalkMap y).commRingCatIsoToRingEquiv).mpr

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, Iff.mpr, IsLocalization.isLocalization_iff_of_ringEquiv, AlgebraicGeometry.IsAffineOpen.fromSpec, Ideal.primeCompl, AlgebraicGeometry.Scheme.Hom.stalkMap, PrimeSpectrum.asIdeal, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
⊢ IsLocalization.AtPrime
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u) y.asIdeal

Tactic:
StructureSheaf.IsLocalization.to_stalk Γ(X, U) y

Premises used: AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, CommRingCat.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
a :
  IsLocalization y.asIdeal.primeCompl (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) ↔
    IsLocalization.AtPrime
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u) y.asIdeal
⊢ IsLocalization y.asIdeal.primeCompl (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)

Tactic:
convert! StructureSheaf.IsLocalization.to_stalk Γ(X, U) y using 1

Premises used: AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, CommRingCat.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
a :
  (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) =
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u) →
    HEq.{u + 1} (α := CommSemiring (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)) CommRing.toCommSemiring (β :=
        CommSemiring (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u))
        CommRing.toCommSemiring →
      RingHom.toAlgebra
          ((asIso (Scheme.Hom.stalkMap hU.fromSpec y)).commRingCatIsoToRingEquiv.toRingHom.comp
            (algebraMap (↑Γ(X, U) : Type u) (↑(X.presheaf.stalk (hU.fromSpec y)) : Type u))) =
        (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U) : Type u) y)).toAlgebra
⊢ IsLocalization y.asIdeal.primeCompl (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) ↔
    IsLocalization y.asIdeal.primeCompl
      (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u)

Tactic:
congr!
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
e_4 :
  (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) =
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u)
e_5 :
  HEq.{u + 1} (α := CommSemiring (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u))
    CommRing.toCommSemiring
a :
  RingHom.toAlgebra (CommRingCat.Hom.hom (Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.germ ⊤ y ⋯)) =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U) : Type u) y)).toAlgebra
⊢ RingHom.toAlgebra
      ((asIso (Scheme.Hom.stalkMap hU.fromSpec y)).commRingCatIsoToRingEquiv.toRingHom.comp
        (algebraMap (↑Γ(X, U) : Type u) (↑(X.presheaf.stalk (hU.fromSpec y)) : Type u))) =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U) : Type u) y)).toAlgebra

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, IsAffineOpen.fromSpec_app_self]

Premises used: CommRingCat.hom_comp, AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
e_4 :
  (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u) =
    (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u)
e_5 :
  HEq.{u + 1} (α := CommSemiring (↑((Spec Γ(X, U)).presheaf.stalk y) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring (↑(TopCat.Presheaf.stalk (TopCat.Sheaf.presheaf (structureSheaf (↑Γ(X, U) : Type u))) y) : Type u))
    CommRing.toCommSemiring
⊢ RingHom.toAlgebra (CommRingCat.Hom.hom (Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.germ ⊤ y ⋯)) =
    (CommRingCat.Hom.hom (StructureSheaf.toStalk (↑Γ(X, U) : Type u) y)).toAlgebra

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
rcases :
  ∀ (x : ↥X) (hx : x ∈ U),
    IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u)
      (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)).asIdeal
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑x : ↥X)) : Type u) (hU.primeIdealOf x).asIdeal

Tactic:
rcases x with ⟨x, hx⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
set :
  let y := hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx);
  ∀ (hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)),
    IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u)
      y.asIdeal
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)).asIdeal

Tactic:
set y := hU.primeIdealOf ⟨x, hx⟩ with hy

Premises used: Subtype.mk, AlgebraicGeometry.IsAffineOpen.primeIdealOf
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum (↑Γ(X, U) : Type u) := hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
⊢ hU.fromSpec y = x

Tactic:
have : hU.fromSpec y = x := hy ▸ hU.fromSpec_primeIdealOf ⟨x, hx⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum (↑Γ(X, U) : Type u) := hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
this : hU.fromSpec y = x
clear_value :
  ∀ (y : PrimeSpectrum (↑Γ(X, U) : Type u)) (hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx))
    (this : hU.fromSpec y = x),
    IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u)
      y.asIdeal
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u) y.asIdeal

Tactic:
clear_value y
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)
this : hU.fromSpec y = x
subst :
  ∀ (hx : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X))
    (hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (hU.fromSpec y) hx)),
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (hU.fromSpec y) hx) : ↥X)) : Type u) y.asIdeal
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X)) : Type u) y.asIdeal

Tactic:
subst this
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hx : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (hU.fromSpec y) hx)
⊢ IsLocalization.AtPrime
    (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (hU.fromSpec y) hx) : ↥X)) : Type u) y.asIdeal

Tactic:
hU.isLocalization_stalk' y hx

Premises used: Set.Mem, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk'
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
y : PrimeSpectrum (↑Γ(X, U) : Type u)
hx : Membership.mem (α := ↥X) U (hU.fromSpec y : ↥X)
hy : y = hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (hU.fromSpec y) hx)
⊢ IsLocalization.AtPrime
    (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (hU.fromSpec y) hx) : ↥X)) : Type u) y.asIdeal

Tactic:
exact hU.isLocalization_stalk' y hx

Premises used: AlgebraicGeometry.IsAffineOpen.isLocalization_stalk'
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Opens ↥Y
hU : IsAffineOpen U
x : ↥X
hx : Membership.mem (α := ↥Y) U (f x : ↥Y)
h :
  ∀ (g : (↑(Y.presheaf.obj (op U)) : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
              (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hx) :
                  (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
                g :
              (↑(Y.presheaf.stalk (f x)) : Type u)) :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      Eq (α := (↑(Y.presheaf.stalk (f x)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hx) :
              (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
            g :
          (↑(Y.presheaf.stalk (f x)) : Type u))
        (0 : (↑(Y.presheaf.stalk (f x)) : Type u))
this : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx)
⊢ ∀ (x_1 : (↑Γ(Y, U) : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
              (a : (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            ((algebraMap (↑Γ(Y, U) : Type u)
                    (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :
                  (a : (↑Γ(Y, U) : Type u)) → (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u))
                x_1 :
              (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u)) :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      Eq (α := (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))
        ((algebraMap (↑Γ(Y, U) : Type u)
                (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :
              (a : (↑Γ(Y, U) : Type u)) → (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u))
            x_1 :
          (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))
        (0 : (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))

Tactic:
h
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Opens ↥Y
hU : IsAffineOpen U
x : ↥X
hx : Membership.mem (α := ↥Y) U (f x : ↥Y)
h :
  ∀ (g : (↑(Y.presheaf.obj (op U)) : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
              (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hx) :
                  (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
                g :
              (↑(Y.presheaf.stalk (f x)) : Type u)) :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      Eq (α := (↑(Y.presheaf.stalk (f x)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hx) :
              (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
            g :
          (↑(Y.presheaf.stalk (f x)) : Type u))
        (0 : (↑(Y.presheaf.stalk (f x)) : Type u))
this : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx)
⊢ ∀ (x_1 : (↑Γ(Y, U) : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
              (a : (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            ((algebraMap (↑Γ(Y, U) : Type u)
                    (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :
                  (a : (↑Γ(Y, U) : Type u)) → (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u))
                x_1 :
              (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u)) :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      Eq (α := (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))
        ((algebraMap (↑Γ(Y, U) : Type u)
                (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :
              (a : (↑Γ(Y, U) : Type u)) → (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u))
            x_1 :
          (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))
        (0 : (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))

Tactic:
exact h
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : (↑Γ(X, U) : Type u)
I : Ideal (↑Γ(X, U) : Type u)
⊢ s ∈ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            s :
          (↑(X.presheaf.stalk x) : Type u))

Tactic:
⟨fun hs x hxU ↦ Ideal.mem_map_of_mem _ hs, fun H ↦ ?_⟩

Premises used: CommRingCat.Hom.hom, Ideal.mem_map_of_mem, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Iff.intro, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : (↑Γ(X, U) : Type u)
I : Ideal (↑Γ(X, U) : Type u)
refine :
  ∀
    (H :
      ∀ (x : ↥X) (h : x ∈ U),
        Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
                (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
              s :
            (↑(X.presheaf.stalk x) : Type u))),
    s ∈ I
⊢ s ∈ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            s :
          (↑(X.presheaf.stalk x) : Type u))

Tactic:
refine ⟨fun hs x hxU ↦ Ideal.mem_map_of_mem _ hs, fun H ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : (↑Γ(X, U) : Type u)
I : Ideal (↑Γ(X, U) : Type u)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
      (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          s :
        (↑(X.presheaf.stalk x) : Type u))
this : (x : ↥(Spec Γ(X, U))) → Algebra (↑Γ(X, U) : Type u) (↑(X.presheaf.stalk (hU.fromSpec x)) : Type u) :=
  fun (x : ↥(Spec Γ(X, U))) ↦
    X.presheaf.algebra_section_stalk
      (((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' : (a : ↥(Spec Γ(X, U))) → ↥(↑U : Scheme)) x)
⊢ ∀ (P : Ideal (↑Γ(X, U) : Type u)) [hP : P.IsPrime],
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP : PrimeSpectrum (↑Γ(X, U) : Type u) })) : Type u) P

Tactic:
have (P : Ideal Γ(X, U)) [hP : P.IsPrime] : IsLocalization.AtPrime _ P :=
      hU.isLocalization_stalk' ⟨P, hP⟩ (hU.isoSpec.inv _).2