awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
H_1 : Y.IsGermInjectiveAt (f x)
V : (↑X.affineOpens : Type u)
hxU : Membership.mem (α := ↥Y) (f ''ᵁ (↑V : X.Opens)) (f x : ↥Y)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
    (↑(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 (f ''ᵁ (↑V : X.Opens)) (f x) hxU)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
hV :
  Eq (α := { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    ((IsOpenImmersion.affineOpensEquiv f :
          (a : (↑X.affineOpens : Type u)) →
            { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
        V :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    (Subtype.mk (p := fun (U : (↑Y.affineOpens : Type u)) ↦ (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f)
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
⊢ X.IsGermInjectiveAt x
have obtain : ∀ (y : ↥X) (hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)) (e : Eq (α := ↥Y) (f y : ↥Y) (f x : ↥Y))
  (H :
    Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
      (↑(Y.presheaf.stalk (f x)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) (Y :=
            Y.presheaf.stalk (f x)) (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f x) sorry)) :
        (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) →
          (↑(Y.presheaf.stalk (f x)) : Type u))),
  X.IsGermInjectiveAt x
Tactic: obtain ⟨y, hy, e : f y = f x⟩ := hxU
Cleared hypotheses: hxU, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
inst : IsOpenImmersion f
H_1 : Y.IsGermInjectiveAt (f x)
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
hV :
  Eq (α := { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    ((IsOpenImmersion.affineOpensEquiv f :
          (a : (↑X.affineOpens : Type u)) →
            { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
        V :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    (Subtype.mk (p := fun (U : (↑Y.affineOpens : Type u)) ↦ (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f)
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
e : Eq (α := ↥Y) (f y : ↥Y) (f x : ↥Y)
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f x)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) (Y := Y.presheaf.stalk (f x))
          (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f x) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
⊢ X.IsGermInjectiveAt x
have obtain : ∀ (H : Y.IsGermInjectiveAt (f y)) (e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y))
  (H :
    Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
      (↑(Y.presheaf.stalk (f y)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) (Y :=
            Y.presheaf.stalk (f y)) (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) sorry)) :
        (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) →
          (↑(Y.presheaf.stalk (f y)) : Type u))),
  X.IsGermInjectiveAt y
Tactic: obtain rfl := f.isOpenEmbedding.injective e
Cleared hypotheses: x, H_1, e, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
hV :
  Eq (α := { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    ((IsOpenImmersion.affineOpensEquiv f :
          (a : (↑X.affineOpens : Type u)) →
            { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
        V :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    (Subtype.mk (p := fun (U : (↑Y.affineOpens : Type u)) ↦ (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f)
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
H_1 : Y.IsGermInjectiveAt (f y)
e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y)
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f y)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) (Y := Y.presheaf.stalk (f y))
          (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f y)) : Type u))
⊢ X.IsGermInjectiveAt y
have refine : Function.Injective (α := (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) (β :=
  (↑(X.presheaf.stalk y) : Type u))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ (↑V : X.Opens) y hy)) :
    (a : (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) → (↑(X.presheaf.stalk y) : Type u))
Tactic: refine ⟨V, hy, V.2, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
hV :
  Eq (α := { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    ((IsOpenImmersion.affineOpensEquiv f :
          (a : (↑X.affineOpens : Type u)) →
            { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
        V :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    (Subtype.mk (p := fun (U : (↑Y.affineOpens : Type u)) ↦ (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f)
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
H_1 : Y.IsGermInjectiveAt (f y)
e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y)
H :
  Function.Injective (α := (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) (β :=
    (↑(Y.presheaf.stalk (f y)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) (Y := Y.presheaf.stalk (f y))
          (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯)) :
      (a : (↑(Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens)))) : Type u)) → (↑(Y.presheaf.stalk (f y)) : Type u))
⊢ Function.Injective (α := (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) (β :=
    (↑(X.presheaf.stalk y) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ (↑V : X.Opens) y hy)) :
      (a : (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) → (↑(X.presheaf.stalk y) : Type u))
have H₁ : MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
  CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens))))
  (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) sorry ≫ Scheme.Hom.stalkMap f y)
Tactic: replace H := ((MorphismProperty.injective CommRingCat).cancel_right_of_respectsIso _
    (f.stalkMap y)).mpr H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
V : (↑X.affineOpens : Type u)
hU : IsAffineOpen (f ''ᵁ (↑V : X.Opens))
hU' : f ''ᵁ (↑V : X.Opens) ≤ Scheme.Hom.opensRange f
hV :
  Eq (α := { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    ((IsOpenImmersion.affineOpensEquiv f :
          (a : (↑X.affineOpens : Type u)) →
            { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
        V :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
    (Subtype.mk (p := fun (U : (↑Y.affineOpens : Type u)) ↦ (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f)
        (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (f ''ᵁ (↑V : X.Opens)) hU) hU' :
      { U : (↑Y.affineOpens : Type u) // (↑U : Y.Opens) ≤ Scheme.Hom.opensRange f })
y : ↥X
hy : y ∈ (↑(↑V : X.Opens) : Set ↥X)
H_1 : Y.IsGermInjectiveAt (f y)
e : Eq (α := ↥Y) (f y : ↥Y) (f y : ↥Y)
H :
  MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) (X := Y.presheaf.obj (Opposite.op (f ''ᵁ (↑V : X.Opens))))
    (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) ⋯ ≫ Scheme.Hom.stalkMap f y)
⊢ Function.Injective (α := (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) (β :=
    (↑(X.presheaf.stalk y) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk y) (X.presheaf.germ (↑V : X.Opens) y hy)) :
      (a : (↑(X.presheaf.obj (Opposite.op (↑V : X.Opens))) : Type u)) → (↑(X.presheaf.stalk y) : Type u))
have H₁ : MorphismProperty.injective CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
  CommRingCat.carrier) (X := Γ(X, (↑V : X.Opens)))
  (CategoryStruct.comp (Y := Γ(Y, f ''ᵁ (↑V : X.Opens))) (Iso.inv (Scheme.Hom.appIso f (↑V : X.Opens)))
    (Y.presheaf.germ (f ''ᵁ (↑V : X.Opens)) (f y) sorry ≫ Scheme.Hom.stalkMap f y))
Tactic: replace H := ((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso
    (f.appIso V).inv _).mpr H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X : Scheme
𝒰 : OpenCover.{u_1, u} X
inst : ∀ (i : 𝒰.I₀), IsGermInjective.{u} (𝒰.X i)
x : ↥X
⊢ X.IsGermInjectiveAt x
have rw : X.IsGermInjectiveAt
  ((𝒰.f (Cover.idx 𝒰 x)) (Exists.choose (p := fun (y : ↥(𝒰.X (Cover.idx 𝒰 x))) ↦ (𝒰.f (Cover.idx 𝒰 x)) y = x) sorry))
Tactic: rw [← (𝒰.covers x).choose_spec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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)
have 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))
Tactic: refine fun p ↦ ⟨?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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)
⊢ ∃ (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))
have 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))
Tactic: obtain ⟨f, hf, H⟩ := H p.asIdeal p.2
-- 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
⊢ ∃ (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))
have refine_1 : IsAffineOpen.{u} (X := Spec R) (PrimeSpectrum.basicOpen f)
Tactic: refine ⟨PrimeSpectrum.basicOpen f, hf, ?_, ?_⟩
-- 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
refine_1 : IsAffineOpen.{u} (X := Spec R) (PrimeSpectrum.basicOpen f)
⊢ ∃ (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))
have 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))
Tactic: refine ⟨PrimeSpectrum.basicOpen f, hf, ?_, ?_⟩
-- 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
⊢ IsAffineOpen.{u} (X := Spec R) (PrimeSpectrum.basicOpen f)
have 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))
Tactic: rw [← basicOpen_eq_of_affine]
-- 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
⊢ 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))
have 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
Tactic: rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
-- 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 : (↑((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))
⊢ x = 0
have 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
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq
    (S := ((Spec.structureSheaf R).obj.obj (.op <| PrimeSpectrum.basicOpen f))) (.powers f) x
Cleared hypotheses: x, hx