awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : ∀ (i : 𝒰.I₀), IsGermInjective.{u} (𝒰.X i)
x : ↥X
⊢ X.IsGermInjectiveAt
    ((𝒰.f (Cover.idx 𝒰 x)) (Exists.choose (p := fun (y : ↥(𝒰.X (Cover.idx 𝒰 x))) ↦ (𝒰.f (Cover.idx 𝒰 x)) y = x) ⋯))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
⊢ IsGermInjective.{u} (Spec R)

Tactic:
fun p ↦ ⟨?_⟩

Premises used: AlgebraicGeometry.Scheme.IsGermInjectiveAt.mk
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
refine :
  ∀ (p : ↥(Spec R)),
    ∃ (U : (Spec R).Opens) (hx : p ∈ U),
      IsAffineOpen U ∧
        Function.Injective (α := (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) (β :=
          (↑((Spec R).presheaf.stalk p) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ U p hx)) :
            (a : (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) → (↑((Spec R).presheaf.stalk p) : Type u))
⊢ IsGermInjective.{u} (Spec R)

Tactic:
refine fun p ↦ ⟨?_⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
obtain :
  ∀ (f : (↑R : Type u)) (hf : f ∉ p.asIdeal)
    (H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0),
    ∃ (U : (Spec R).Opens) (hx : p ∈ U),
      IsAffineOpen U ∧
        Function.Injective (α := (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) (β :=
          (↑((Spec R).presheaf.stalk p) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ U p hx)) :
            (a : (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) → (↑((Spec R).presheaf.stalk p) : Type u))
⊢ ∃ (U : (Spec R).Opens) (hx : p ∈ U),
    IsAffineOpen U ∧
      Function.Injective (α := (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) (β :=
        (↑((Spec R).presheaf.stalk p) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ U p hx)) :
          (a : (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) → (↑((Spec R).presheaf.stalk p) : Type u))

Tactic:
obtain ⟨f, hf, H⟩ := H p.asIdeal p.2

Premises used: PrimeSpectrum.isPrime, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
⊢ ∃ (U : (Spec R).Opens) (hx : p ∈ U),
    IsAffineOpen U ∧
      Function.Injective (α := (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) (β :=
        (↑((Spec R).presheaf.stalk p) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ U p hx)) :
          (a : (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) → (↑((Spec R).presheaf.stalk p) : Type u))

Tactic:
⟨PrimeSpectrum.basicOpen f, hf, ?_, ?_⟩

Premises used: PrimeSpectrum.basicOpen, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
refine_1 : IsAffineOpen.{u} (X := Spec R) (PrimeSpectrum.basicOpen f)
refine_2 :
  Function.Injective (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) (β :=
    (↑((Spec R).presheaf.stalk p) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := (Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) (Y :=
          (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) :
      (a : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) →
        (↑((Spec R).presheaf.stalk p) : Type u))
⊢ ∃ (U : (Spec R).Opens) (hx : p ∈ U),
    IsAffineOpen U ∧
      Function.Injective (α := (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) (β :=
        (↑((Spec R).presheaf.stalk p) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ U p hx)) :
          (a : (↑((Spec R).presheaf.obj (Opposite.op U)) : Type u)) → (↑((Spec R).presheaf.stalk p) : Type u))

Tactic:
refine ⟨PrimeSpectrum.basicOpen f, hf, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
refine_1 :
  IsAffineOpen.{u} (X := Spec R)
    ((Spec R).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (ΓSpecIso R).inv :
          (a : (↑R : Type u)) → (↑Γ(Spec R, ⊤) : Type u))
        f))
⊢ IsAffineOpen.{u} (X := Spec R) (PrimeSpectrum.basicOpen f)

Tactic:
rw [← basicOpen_eq_of_affine]

Premises used: AlgebraicGeometry.basicOpen_eq_of_affine
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
⊢ IsAffineOpen.{u} (X := Spec R)
    ((Spec R).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (ΓSpecIso R).inv :
          (a : (↑R : Type u)) → (↑Γ(Spec R, ⊤) : Type u))
        f))

Tactic:
(isAffineOpen_top (Spec R)).basicOpen _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Spec, AlgebraicGeometry.IsAffineOpen.basicOpen
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
⊢ IsAffineOpen.{u} (X := Spec R)
    ((Spec R).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (ΓSpecIso R).inv :
          (a : (↑R : Type u)) → (↑Γ(Spec R, ⊤) : Type u))
        f))

Tactic:
exact (isAffineOpen_top (Spec R)).basicOpen _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Spec, AlgebraicGeometry.IsAffineOpen.basicOpen
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
refine_2 :
  ∀ (x : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)),
    Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := (Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) (Y :=
                (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf) :
              (a : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) →
                (↑((Spec R).presheaf.stalk p) : Type u))
            x :
          (↑((Spec R).presheaf.stalk p) : Type u))
        (0 : (↑((Spec R).presheaf.stalk p) : Type u)) →
      x = 0
⊢ Function.Injective (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) (β :=
    (↑((Spec R).presheaf.stalk p) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := (Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) (Y :=
          (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf)) :
      (a : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) →
        (↑((Spec R).presheaf.stalk p) : Type u))

Tactic:
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]

Premises used: RingHom.ker_eq_bot_iff_eq_zero, RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
x : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)
hx :
  Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := (Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) (Y :=
            (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf) :
          (a : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) →
            (↑((Spec R).presheaf.stalk p) : Type u))
        x :
      (↑((Spec R).presheaf.stalk p) : Type u))
    (0 : (↑((Spec R).presheaf.stalk p) : Type u))
refine_2 :
  ∀ (x : (↑R : Type u)) (s : ↥(Submonoid.powers f))
    (hx :
      Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := (Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) (Y :=
                (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf) :
              (a : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) →
                (↑((Spec R).presheaf.stalk p) : Type u))
            (IsLocalization.mk'
              (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                      (Spec.structureSheaf (↑R : Type u)))
                    (Opposite.op (PrimeSpectrum.basicOpen f))) :
                Type u)
              x s) :
          (↑((Spec R).presheaf.stalk p) : Type u))
        (0 : (↑((Spec R).presheaf.stalk p) : Type u))),
    Eq (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
      (IsLocalization.mk'
        (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (Spec.structureSheaf (↑R : Type u)))
              (Opposite.op (PrimeSpectrum.basicOpen f))) :
          Type u)
        x s)
      0
⊢ x = 0

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq
    (S := ((Spec.structureSheaf R).obj.obj (.op <| PrimeSpectrum.basicOpen f))) (.powers f) x

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
x : (↑R : Type u)
s : ↥(Submonoid.powers f)
hx :
  Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := (Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) (Y :=
            (Spec R).presheaf.stalk p) ((Spec R).presheaf.germ (PrimeSpectrum.basicOpen f) p hf) :
          (a : (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u)) →
            (↑((Spec R).presheaf.stalk p) : Type u))
        ((algebraMap (↑R : Type u)
                (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                        (Spec.structureSheaf (↑R : Type u)))
                      (Opposite.op (PrimeSpectrum.basicOpen f))) :
                  Type u) :
              (a : (↑R : Type u)) →
                (↑((Spec.structureSheaf (↑R : Type u)).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
            x :
          (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                  (Spec.structureSheaf (↑R : Type u)))
                (Opposite.op (PrimeSpectrum.basicOpen f))) :
            Type u)) :
      (↑((Spec R).presheaf.stalk p) : Type u))
    (0 : (↑((Spec R).presheaf.stalk p) : Type u))
⊢ Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (StructureSheaf.toStalk (↑R : Type u) p) :
          (a : (↑R : Type u)) → (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk p) : Type u))
        x :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u)) p) : Type u))
    (0 : (↑((Spec R).presheaf.stalk p) : Type u))

Tactic:
erw [elementwise_of% StructureSheaf.algebraMap_germ] at hx

Premises used: AlgebraicGeometry.StructureSheaf.algebraMap_germ
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
x : (↑R : Type u)
s : ↥(Submonoid.powers f)
hx :
  Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (StructureSheaf.toStalk (↑R : Type u) p) :
          (a : (↑R : Type u)) → (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk p) : Type u))
        x :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u)) p) : Type u))
    (0 : (↑((Spec R).presheaf.stalk p) : Type u))
refine_2 :
  ∀ (y : (↑R : Type u)) (hy : y ∈ p.asIdeal.primeCompl)
    (hy' : (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ p.asIdeal.primeCompl) y hy) : (↑R : Type u)) * x = 0),
    Eq (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
      (IsLocalization.mk'
        (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (Spec.structureSheaf (↑R : Type u)))
              (Opposite.op (PrimeSpectrum.basicOpen f))) :
          Type u)
        x s)
      0
⊢ Eq (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
    (IsLocalization.mk'
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (Spec.structureSheaf (↑R : Type u)))
            (Opposite.op (PrimeSpectrum.basicOpen f))) :
        Type u)
      x s)
    0

Tactic:
obtain ⟨⟨y, hy⟩, hy'⟩ := (IsLocalization.map_eq_zero_iff p.asIdeal.primeCompl
    ((Spec.structureSheaf R).presheaf.stalk p) _).mp hx

Premises used: CommRingCat.carrier, IsLocalization.map_eq_zero_iff, TopCat.Presheaf.stalk, Iff.mp, AlgebraicGeometry.Spec.structureSheaf, Ideal.primeCompl, TopCat.Sheaf.presheaf, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
x : (↑R : Type u)
s : ↥(Submonoid.powers f)
hx :
  Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (StructureSheaf.toStalk (↑R : Type u) p) :
          (a : (↑R : Type u)) → (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk p) : Type u))
        x :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u)) p) : Type u))
    (0 : (↑((Spec R).presheaf.stalk p) : Type u))
y : (↑R : Type u)
hy : y ∈ p.asIdeal.primeCompl
hy' : (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ p.asIdeal.primeCompl) y hy) : (↑R : Type u)) * x = 0
refine_2 :
  ∀ (n : ℕ) (hn : f ^ n * x = 0),
    Eq (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
      (IsLocalization.mk'
        (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
                (Spec.structureSheaf (↑R : Type u)))
              (Opposite.op (PrimeSpectrum.basicOpen f))) :
          Type u)
        x s)
      0
⊢ Eq (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
    (IsLocalization.mk'
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (Spec.structureSheaf (↑R : Type u)))
            (Opposite.op (PrimeSpectrum.basicOpen f))) :
        Type u)
      x s)
    0

Tactic:
obtain ⟨n, hn⟩ := H x y hy' hy
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
x : (↑R : Type u)
s : ↥(Submonoid.powers f)
hx :
  Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (StructureSheaf.toStalk (↑R : Type u) p) :
          (a : (↑R : Type u)) → (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk p) : Type u))
        x :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u)) p) : Type u))
    (0 : (↑((Spec R).presheaf.stalk p) : Type u))
y : (↑R : Type u)
hy : y ∈ p.asIdeal.primeCompl
hy' : (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ p.asIdeal.primeCompl) y hy) : (↑R : Type u)) * x = 0
n : ℕ
hn : f ^ n * x = 0
⊢ Eq (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
    (IsLocalization.mk'
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (Spec.structureSheaf (↑R : Type u)))
            (Opposite.op (PrimeSpectrum.basicOpen f))) :
        Type u)
      x s)
    0

Tactic:
(@IsLocalization.mk'_eq_zero_iff ..).mpr ?_

Premises used: Iff.mpr, Set.Mem, IsLocalization.mk'_eq_zero_iff
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
R : CommRingCat
H_1 :
  ∀ (I : Ideal (↑R : Type u)),
    I.IsPrime → ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
p : ↥(Spec R)
f : (↑R : Type u)
hf : f ∉ p.asIdeal
H : ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ p.asIdeal → ∃ (n : ℕ), f ^ n * x = 0
x : (↑R : Type u)
s : ↥(Submonoid.powers f)
hx :
  Eq (α := (↑((Spec R).presheaf.stalk p) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (StructureSheaf.toStalk (↑R : Type u) p) :
          (a : (↑R : Type u)) → (↑((structurePresheafInCommRingCat (↑R : Type u)).stalk p) : Type u))
        x :
      (↑(TopCat.Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u)) p) : Type u))
    (0 : (↑((Spec R).presheaf.stalk p) : Type u))
y : (↑R : Type u)
hy : y ∈ p.asIdeal.primeCompl
hy' : (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ p.asIdeal.primeCompl) y hy) : (↑R : Type u)) * x = 0
n : ℕ
hn : f ^ n * x = 0
refine_2 : ∃ (m : ↥(Submonoid.powers f)), (↑m : (↑R : Type u)) * x = 0
⊢ Eq (α := (↑((Spec R).presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f))) : Type u))
    (IsLocalization.mk'
      (↑(Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u)) : Type u)))
              (Spec.structureSheaf (↑R : Type u)))
            (Opposite.op (PrimeSpectrum.basicOpen f))) :
        Type u)
      x s)
    0

Tactic:
refine (@IsLocalization.mk'_eq_zero_iff ..).mpr ?_

Premises used: Iff.mpr, IsLocalization.mk'_eq_zero_iff