awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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.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
have 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))
Tactic: erw [elementwise_of% StructureSheaf.algebraMap_germ] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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))
⊢ 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
have 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
Tactic: obtain ⟨⟨y, hy⟩, hy'⟩ := (IsLocalization.map_eq_zero_iff p.asIdeal.primeCompl
    ((Spec.structureSheaf R).presheaf.stalk p) _).mp hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨n, hn⟩ := H x y hy' hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
have refine_2 : ∃ (m : ↥(Submonoid.powers f)), (↑m : (↑R : Type u)) * x = 0
Tactic: refine (@IsLocalization.mk'_eq_zero_iff ..).mpr ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsIntegral X
⊢ X.IsGermInjective
have 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 sorry)) :
      (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: refine fun x ↦ ⟨⟨(X.affineCover.f _).opensRange, X.affineCover.covers x,
    (isAffineOpen_opensRange (X.affineCover.f _)), ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsIntegral X
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))
have 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)
Tactic: have : Nonempty (X.affineCover.f _).opensRange := ⟨⟨_, X.affineCover.covers x⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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)
⊢ 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))
have 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 sorry) :
          ↥X)) :
    Type u)
  (PrimeSpectrum.asIdeal
    (IsAffineOpen.primeIdealOf sorry
      (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 sorry)))
Tactic: have := (isAffineOpen_opensRange (X.affineCover.f _)).isLocalization_stalk
    ⟨_, X.affineCover.covers x⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
have refine : ∀ (i : X.affineOpenCover.openCover.I₀), IsNoetherianRing.{u} (↑(X.affineOpenCover.X (P := IsOpenImmersion) i) : Type u)
Tactic: refine @Scheme.IsGermInjective.of_openCover _ (X.affineOpenCover.openCover) (fun i ↦ this _ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
f : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R A : CommRingCat
inst : IsLocallyNoetherian X
⊢ X.IsGermInjective
have suffices : ∀ (R : CommRingCat.{u}), IsNoetherianRing.{u} (↑R : Type u) → Scheme.IsGermInjective.{u} (Spec R)
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))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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)
have 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
Tactic: refine fun R hR ↦ Scheme.IsGermInjective.Spec fun I hI ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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))
⊢ ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
have hJ : ∀ (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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
have 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
Tactic: choose f hf using fun x ↦ (hJ x).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
have 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
Tactic: obtain ⟨s, hs⟩ := (isNoetherianRing_iff_ideal_fg R).mp ‹_› J
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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
⊢ ∃ f ∉ I, ∀ (x y : (↑R : Type u)), y * x = 0 → y ∉ I → ∃ (n : ℕ), f ^ n * x = 0
have hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
Tactic: have hs' : (s : Set R) ⊆ J := hs ▸ Ideal.subset_span
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
have 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)) sorry) : (↑R : Type u)) 1 * x = 0
Tactic: refine ⟨_, (s.attach.prod fun x ↦ f x (hs' x.2)).2, fun x y e hy ↦ ⟨1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ HPow.hPow (α := (↑R : Type u)) (β := ℕ) (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u)) 1 * x = 0
have rw : Membership.mem (γ := Ideal (↑R : Type u))
  (Submodule.annihilator (M := (↑R : Type u))
    ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) sorry) : (↑R : Type u))))
  x
Tactic: rw [pow_one, mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
have refine : J ≤
  Submodule.annihilator (M := (↑R : Type u))
    ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) sorry) : (↑R : Type u)))
Tactic: refine SetLike.le_def.mp ?_ ((hJ x).mpr ⟨⟨y, hy⟩, e⟩)