awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∃ (m : ↥(Submonoid.powers f)), (↑m : (↑R : Type u)) * x = 0

Tactic:
⟨⟨_, n, rfl⟩, hn⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- 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
⊢ ∃ (m : ↥(Submonoid.powers f)), (↑m : (↑R : Type u)) * x = 0

Tactic:
exact ⟨⟨_, n, rfl⟩, hn⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsIntegral X
⊢ X.IsGermInjective

Tactic:
fun x ↦ ⟨⟨(X.affineCover.f _).opensRange, X.affineCover.covers x,
    (isAffineOpen_opensRange (X.affineCover.f _)), ?_⟩⟩

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.IsGermInjectiveAt.mk, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.Scheme.Cover.covers, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Cover.idx, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsIntegral X
refine :
  ∀ (x : ↥X),
    Function.Injective (α :=
      (↑(X.presheaf.obj
            (Opposite.op
              (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
                (X.affineCover.f (Scheme.Cover.idx X.affineCover 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) (X :=
            X.presheaf.obj
              (Opposite.op
                (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
                  (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))))
            (Y := X.presheaf.stalk x)
            (X.presheaf.germ
              (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
                (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
              x ⋯)) :
        (a :
            (↑(X.presheaf.obj
                  (Opposite.op (Scheme.Hom.opensRange (X.affineCover.f (Scheme.Cover.idx X.affineCover x))))) :
              Type u)) →
          (↑(X.presheaf.stalk x) : Type u))
⊢ X.IsGermInjective

Tactic:
refine fun x ↦ ⟨⟨(X.affineCover.f _).opensRange, X.affineCover.covers x,
    (isAffineOpen_opensRange (X.affineCover.f _)), ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsIntegral X
x : ↥X
⊢ Nonempty.{u + 1}
    ↥(↑(Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
            (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) :
        Scheme)

Tactic:
have : Nonempty (X.affineCover.f _).opensRange := ⟨⟨_, X.affineCover.covers x⟩⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsIntegral X
x : ↥X
this :
  Nonempty.{u + 1}
    ↥(↑(Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
            (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) :
        Scheme)
⊢ IsLocalization.AtPrime (R :=
    (↑Γ(X,
          Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
            (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) :
      Type u))
    (↑(X.presheaf.stalk
          (↑(Subtype.mk (p := fun (x_1 : ↥X) ↦
                x_1 ∈
                  Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
                    (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
                x ⋯) :
            ↥X)) :
      Type u)
    (PrimeSpectrum.asIdeal
      (IsAffineOpen.primeIdealOf ⋯
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
          x_1 ∈
            Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
              (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
          x ⋯)))

Tactic:
have := (isAffineOpen_opensRange (X.affineCover.f _)).isLocalization_stalk
    ⟨_, X.affineCover.covers x⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsIntegral X
x : ↥X
this_1 :
  Nonempty.{u + 1}
    ↥(↑(Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
            (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) :
        Scheme)
this :
  IsLocalization.AtPrime (R :=
    (↑Γ(X,
          Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
            (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) :
      Type u))
    (↑(X.presheaf.stalk
          (↑(Subtype.mk (p := fun (x_1 : ↥X) ↦
                x_1 ∈
                  Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
                    (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
                x ⋯) :
            ↥X)) :
      Type u)
    (PrimeSpectrum.asIdeal
      (IsAffineOpen.primeIdealOf ⋯
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
          x_1 ∈
            Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
              (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
          x ⋯)))
⊢ Function.Injective (α :=
    (↑(X.presheaf.obj
          (Opposite.op
            (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
              (X.affineCover.f (Scheme.Cover.idx X.affineCover 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) (X :=
          X.presheaf.obj
            (Opposite.op
              (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
                (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))))
          (Y := X.presheaf.stalk x)
          (X.presheaf.germ
            (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
              (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
            x ⋯)) :
      (a :
          (↑(X.presheaf.obj
                (Opposite.op (Scheme.Hom.opensRange (X.affineCover.f (Scheme.Cover.idx X.affineCover x))))) :
            Type u)) →
        (↑(X.presheaf.stalk x) : Type u))

Tactic:
@IsLocalization.injective _ _ _ _ _ (show _ from _) this
    (Ideal.primeCompl_le_nonZeroDivisors _)

Premises used: IsLocalization.injective, Ideal.primeCompl_le_nonZeroDivisors
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsIntegral X
x : ↥X
this_1 :
  Nonempty.{u + 1}
    ↥(↑(Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
            (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) :
        Scheme)
this :
  IsLocalization.AtPrime (R :=
    (↑Γ(X,
          Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
            (X.affineCover.f (Scheme.Cover.idx X.affineCover x))) :
      Type u))
    (↑(X.presheaf.stalk
          (↑(Subtype.mk (p := fun (x_1 : ↥X) ↦
                x_1 ∈
                  Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
                    (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
                x ⋯) :
            ↥X)) :
      Type u)
    (PrimeSpectrum.asIdeal
      (IsAffineOpen.primeIdealOf ⋯
        (Subtype.mk (p := fun (x_1 : ↥X) ↦
          x_1 ∈
            Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
              (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
          x ⋯)))
⊢ Function.Injective (α :=
    (↑(X.presheaf.obj
          (Opposite.op
            (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
              (X.affineCover.f (Scheme.Cover.idx X.affineCover 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) (X :=
          X.presheaf.obj
            (Opposite.op
              (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
                (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))))
          (Y := X.presheaf.stalk x)
          (X.presheaf.germ
            (Scheme.Hom.opensRange (X := X.affineCover.X (Scheme.Cover.idx X.affineCover x))
              (X.affineCover.f (Scheme.Cover.idx X.affineCover x)))
            x ⋯)) :
      (a :
          (↑(X.presheaf.obj
                (Opposite.op (Scheme.Hom.opensRange (X.affineCover.f (Scheme.Cover.idx X.affineCover x))))) :
            Type u)) →
        (↑(X.presheaf.stalk x) : Type u))

Tactic:
exact @IsLocalization.injective _ _ _ _ _ (show _ from _) this
    (Ideal.primeCompl_le_nonZeroDivisors _)

Premises used: IsLocalization.injective, Ideal.primeCompl_le_nonZeroDivisors
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsLocallyNoetherian X
this : ∀ (R : CommRingCat.{u}), IsNoetherianRing.{u} (↑R : Type u) → Scheme.IsGermInjective.{u} (Spec R)
⊢ X.IsGermInjective

Tactic:
@Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)

Premises used: AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.IsGermInjective.of_openCover, AlgebraicGeometry.Scheme.affineOpenCover
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsLocallyNoetherian X
this : ∀ (R : CommRingCat.{u}), IsNoetherianRing.{u} (↑R : Type u) → Scheme.IsGermInjective.{u} (Spec R)
refine :
  ∀ (i : X.affineOpenCover.openCover.I₀),
    IsNoetherianRing.{u} (↑(X.affineOpenCover.X (P := IsOpenImmersion) i) : Type u)
⊢ X.IsGermInjective

Tactic:
refine @Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)

Premises used: AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.IsGermInjective.of_openCover, AlgebraicGeometry.Scheme.affineOpenCover
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsLocallyNoetherian X
this : ∀ (R : CommRingCat.{u}), IsNoetherianRing.{u} (↑R : Type u) → Scheme.IsGermInjective.{u} (Spec R)
i : X.affineOpenCover.openCover.I₀
⊢ IsNoetherianRing.{u} (↑(X.affineOpenCover.X (P := IsOpenImmersion) i) : Type u)

Tactic:
isLocallyNoetherian_Spec.mp
      (isLocallyNoetherian_of_isOpenImmersion (X.affineOpenCover.f i))

Premises used: AlgebraicGeometry.Scheme.AffineCover.f, AlgebraicGeometry.isLocallyNoetherian_Spec, AlgebraicGeometry.Scheme.affineOpenCover, Iff.mp, AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsLocallyNoetherian X
this : ∀ (R : CommRingCat.{u}), IsNoetherianRing.{u} (↑R : Type u) → Scheme.IsGermInjective.{u} (Spec R)
i : X.affineOpenCover.openCover.I₀
⊢ IsNoetherianRing.{u} (↑(X.affineOpenCover.X (P := IsOpenImmersion) i) : Type u)

Tactic:
exact isLocallyNoetherian_Spec.mp
      (isLocallyNoetherian_of_isOpenImmersion (X.affineOpenCover.f i))

Premises used: AlgebraicGeometry.Scheme.AffineCover.f, AlgebraicGeometry.isLocallyNoetherian_Spec, AlgebraicGeometry.Scheme.affineOpenCover, Iff.mp, AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsLocallyNoetherian X
suffices : ∀ (R : CommRingCat.{u}), IsNoetherianRing.{u} (↑R : Type u) → Scheme.IsGermInjective.{u} (Spec R)
⊢ X.IsGermInjective

Tactic:
suffices ∀ (R : CommRingCat.{u}) (_ : IsNoetherianRing R), (Spec R).IsGermInjective by
    refine @Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)
    exact isLocallyNoetherian_Spec.mp
      (isLocallyNoetherian_of_isOpenImmersion (X.affineOpenCover.f i))
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsLocallyNoetherian X
⊢ ∀ (R : CommRingCat.{u}), IsNoetherianRing.{u} (↑R : Type u) → Scheme.IsGermInjective.{u} (Spec R)

Tactic:
fun R hR ↦ Scheme.IsGermInjective.Spec fun I hI ↦ ?_

Premises used: AlgebraicGeometry.Scheme.IsGermInjective.Spec
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsLocallyNoetherian X
refine :
  ∀ (R : CommRingCat.{u}) (hR : IsNoetherianRing.{u} (↑R : Type u)) (I : Ideal (↑R : Type u)) (hI : I.IsPrime),
    ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
⊢ ∀ (R : CommRingCat.{u}), IsNoetherianRing.{u} (↑R : Type u) → Scheme.IsGermInjective.{u} (Spec R)

Tactic:
refine fun R hR ↦ Scheme.IsGermInjective.Spec fun I hI ↦ ?_

Premises used: AlgebraicGeometry.Scheme.IsGermInjective.Spec
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
⊢ ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0

Tactic:
have hJ (x) : x ∈ J ↔ ∃ y : I.primeCompl, y * x = 0 :=
    IsLocalization.map_eq_zero_iff I.primeCompl _ x
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
choose :
  ∀ (f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl)
    (hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0),
    ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
⊢ ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0

Tactic:
choose f hf using fun x ↦ (hJ x).mp

Premises used: Iff.mp
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
obtain :
  ∀ (s : Finset (↑R : Type u)) (hs : Ideal.span (↑s : Set (↑R : Type u)) = J),
    ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
⊢ ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0

Tactic:
obtain ⟨s, hs⟩ := (isNoetherianRing_iff_ideal_fg R).mp ‹_› J

Premises used: CommRingCat.carrier, isNoetherianRing_iff_ideal_fg, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
⊢ (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))

Tactic:
have hs' : (s : Set R) ⊆ J := hs ▸ Ideal.subset_span
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
⊢ ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0

Tactic:
⟨_, (s.attach.prod fun x ↦ f x (hs' x.2)).2, fun x y e hy ↦ ⟨1, ?_⟩⟩

Premises used: Finset.prod, And.intro, Finset.attach, Exists.intro, OfNat.ofNat, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
refine :
  ∀ (x y : (↑R : Type u)) (e : y * x = 0) (hy : y ∉ I),
    HPow.hPow (α := (↑R : Type u)) (β := ℕ) (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u)) 1 * x = 0
⊢ ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0

Tactic:
refine ⟨_, (s.attach.prod fun x ↦ f x (hs' x.2)).2, fun x y e hy ↦ ⟨1, ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
x y : (↑R : Type u)
e : y * x = 0
hy : y ∉ I
rw :
  Membership.mem (γ := Ideal (↑R : Type u))
    (Submodule.annihilator (M := (↑R : Type u))
      ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u))))
    x
⊢ HPow.hPow (α := (↑R : Type u)) (β := ℕ) (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u)) 1 * x = 0

Tactic:
rw [pow_one, mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton]

Premises used: pow_one, mul_comm, smul_eq_mul, Submodule.mem_annihilator_span_singleton
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
x y : (↑R : Type u)
e : y * x = 0
hy : y ∉ I
⊢ Membership.mem (γ := Ideal (↑R : Type u))
    (Submodule.annihilator (M := (↑R : Type u))
      ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u))))
    x

Tactic:
SetLike.le_def.mp ?_ ((hJ x).mpr ⟨⟨y, hy⟩, e⟩)

Premises used: Iff.mpr, SetLike.le_def, Subtype.mk, Exists.intro, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
x y : (↑R : Type u)
e : y * x = 0
hy : y ∉ I
refine :
  J ≤
    Submodule.annihilator (M := (↑R : Type u))
      ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u)))
⊢ Membership.mem (γ := Ideal (↑R : Type u))
    (Submodule.annihilator (M := (↑R : Type u))
      ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u))))
    x

Tactic:
refine SetLike.le_def.mp ?_ ((hJ x).mpr ⟨⟨y, hy⟩, e⟩)

Premises used: Iff.mpr, SetLike.le_def, Subtype.mk, Exists.intro, Iff.mp