awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
refine_1 : Eq (α := ↥S) (sX x : ↥S) ((φ ≫ sY) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥S)
refine_1₁ :
  Eq (α := ↥S) (sX x : ↥S) ((X.fromSpecStalk x ≫ sX) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥S)
⊢ Eq (α := ↥S) (sX x : ↥S) (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y) : ↥S)
have refine_1₂ : Eq (α := ↥S) (sX x : ↥S) (sX ((X.fromSpecStalk x) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X) : ↥S)
Tactic: rw [← Scheme.Hom.comp_apply, h, Scheme.Hom.comp_apply, Scheme.fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
refine_1 : Eq (α := ↥S) (sX x : ↥S) ((φ ≫ sY) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥S)
refine_1₁ :
  Eq (α := ↥S) (sX x : ↥S) ((X.fromSpecStalk x ≫ sX) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥S)
refine_1₂ :
  Eq (α := ↥S) (sX x : ↥S)
    (sX ((X.fromSpecStalk x) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X) : ↥S)
⊢ Eq (α := ↥S) (sX x : ↥S) (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y) : ↥S)
have refine_1₃ : Eq (α := ↥S) (sX x : ↥S) (sX x : ↥S)
Tactic: rw [← Scheme.Hom.comp_apply, h, Scheme.Hom.comp_apply, Scheme.fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Eq (α :=
    S.presheaf.stalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y)) ⟶ X.presheaf.stalk x)
    (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) ≫
      Scheme.stalkClosedPointTo φ)
    (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x)
have refine_2 : Eq (α :=
  Spec (X.presheaf.stalk x) ⟶
    Spec (S.presheaf.stalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y))))
  (Spec.map
    (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) ≫
      Scheme.stalkClosedPointTo φ))
  (Spec.map (S.presheaf.stalkSpecializes sorry ≫ Scheme.Hom.stalkMap sX x))
Tactic: apply Spec.map_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Eq (α :=
    Spec (X.presheaf.stalk x) ⟶
      Spec (S.presheaf.stalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y))))
    (Spec.map
      (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) ≫
        Scheme.stalkClosedPointTo φ))
    (Spec.map (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x))
have refine_2 : CategoryStruct.comp (Y :=
    Spec (S.presheaf.stalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y))))
    (Spec.map
      (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) ≫
        Scheme.stalkClosedPointTo φ))
    (S.fromSpecStalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y))) =
  CategoryStruct.comp (Y :=
    Spec (S.presheaf.stalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y))))
    (Spec.map (S.presheaf.stalkSpecializes sorry ≫ Scheme.Hom.stalkMap sX x))
    (S.fromSpecStalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y)))
Tactic: rw [← cancel_mono (S.fromSpecStalk _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
have obtain : ∀ (U' : Opens ↥X) (h₁ : U' ∈ X.affineOpens) (h₂ : x ∈ U') (h₃ : U' ≤ U ⊓ V), hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
Tactic: obtain ⟨U', h₁, h₂, h₃ : U' ≤ U ⊓ V⟩ :=
    Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens (show x ∈ U ⊓ V from ⟨hxU, hxV⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
have transitivity : hU.fromSpecStalk hxU = fromSpecStalk h₁ h₂
Tactic: transitivity fromSpecStalk h₁ h₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
transitivity : hU.fromSpecStalk hxU = fromSpecStalk h₁ h₂
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
have transitivity₁ : fromSpecStalk h₁ h₂ = hV.fromSpecStalk hxV
Tactic: transitivity fromSpecStalk h₁ h₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
    (Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁)
have rw : Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
  (Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE sorry).op) ≫ hU.fromSpec)
Tactic: rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
rw :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
    (Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hU.fromSpec)
⊢ Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
    (Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁)
have rw₁ : Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
  (Spec.map (X.presheaf.map (homOfLE sorry).op ≫ X.presheaf.germ U' x h₂) ≫ hU.fromSpec)
Tactic: rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
rw :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
    (Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hU.fromSpec)
rw₁ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
    (Spec.map (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.germ U' x h₂) ≫ hU.fromSpec)
⊢ Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
    (Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁)
have rw₂ : Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec)
  (Spec.map (X.presheaf.germ U x sorry) ≫ hU.fromSpec)
Tactic: rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁)
    (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
have rw : Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
  (Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE sorry).op) ≫ hV.fromSpec)
  (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
Tactic: rw [← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
rw :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    (Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hV.fromSpec)
    (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
⊢ Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁)
    (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
have rw₁ : Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
  (Spec.map (X.presheaf.map (homOfLE sorry).op ≫ X.presheaf.germ U' x h₂) ≫ hV.fromSpec)
  (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
Tactic: rw [← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
rw :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    (Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hV.fromSpec)
    (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
rw₁ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    (Spec.map (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.germ U' x h₂) ≫ hV.fromSpec)
    (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
⊢ Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U' x h₂) ≫ fromSpec h₁)
    (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
have rw₂ : Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ V x sorry) ≫ hV.fromSpec)
  (Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec)
Tactic: rw [← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (hypothesis)
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
U_1 V : X_1.Opens
hU_1 : IsAffineOpen U_1
hV : IsAffineOpen V
X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hx : x ∈ U
⊢ IsPreimmersion (X := Spec (X.presheaf.stalk x)) (Spec.map (X.presheaf.germ U x hx) ≫ hU.fromSpec)
have this : IsPreimmersion (X := Spec (X.presheaf.stalk x)) (Spec.map (X.presheaf.germ U x hx))
Tactic: haveI : IsPreimmersion (Spec.map (X.presheaf.germ U x hx)) :=
    letI : Algebra Γ(X, U) (X.presheaf.stalk x) := (X.presheaf.germ U x hx).hom.toAlgebra
    haveI := hU.isLocalization_stalk ⟨x, hx⟩
    IsPreimmersion.of_isLocalization (R := Γ(X, U)) (S := X.presheaf.stalk x)
      (hU.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hxU : x ∈ U
⊢ hU.fromSpec
      ((Spec.map (X.presheaf.germ U x hxU)) (closedPoint (↑(X.presheaf.stalk x) : Type u)) :
        ↥(Spec (X.presheaf.obj (op U)))) =
    x
have rw : hU.fromSpec (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)) = x
Tactic: rw [← hU.primeIdealOf_eq_map_closedPoint ⟨x, hxU⟩, hU.fromSpec_primeIdealOf ⟨x, hxU⟩]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : Opens ↥X
hU : IsAffineOpen U
x : ↥X
hxU : x ∈ U
rw : hU.fromSpec (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)) = x
⊢ hU.fromSpec
      ((Spec.map (X.presheaf.germ U x hxU)) (closedPoint (↑(X.presheaf.stalk x) : Type u)) :
        ↥(Spec (X.presheaf.obj (op U)))) =
    x
have rw₁ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) : ↥X) = x
Tactic: rw [← hU.primeIdealOf_eq_map_closedPoint ⟨x, hxU⟩, hU.fromSpec_primeIdealOf ⟨x, hxU⟩]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Hom.app (X.fromSpecStalk x) U =
    X.presheaf.germ U x hxU ≫
      Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ (Spec (X.presheaf.stalk x)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))
have obtain : ∀ (V : X.Opens) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X)) (hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)),
  Hom.app (X.fromSpecStalk x) U =
    X.presheaf.germ U x hxU ≫
      Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ (Spec (X.presheaf.stalk x)).presheaf.map (Quiver.Hom.op (homOfLE sorry))
Tactic: obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    hxU U.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
V : X.Opens
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ Hom.app (X.fromSpecStalk x) U =
    X.presheaf.germ U x hxU ≫
      Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ (Spec (X.presheaf.stalk x)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))
have rw : Eq (α := Γ(X, U) ⟶ Γ(Spec (X.presheaf.stalk x), (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ⁻¹ᵁ U))
  ((X.presheaf.map (homOfLE hVU).op ≫
        Iso.inv (ΓSpecIso Γ(X, V)) ≫ (Spec Γ(X, V)).presheaf.map (Quiver.Hom.op (homOfLE sorry))) ≫
      Hom.app (Spec.map (X.presheaf.germ V x hxV)) (IsAffineOpen.fromSpec hV ⁻¹ᵁ U) :
    Γ(X, U) ⟶ Γ(Spec (X.presheaf.stalk x), Spec.map (X.presheaf.germ V x hxV) ⁻¹ᵁ IsAffineOpen.fromSpec hV ⁻¹ᵁ U))
  ((X.presheaf.map (homOfLE hVU).op ≫ X.presheaf.germ V x hxV) ≫
    Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ (Spec (X.presheaf.stalk x)).presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [← hV.fromSpecStalk_eq_fromSpecStalk hxV, IsAffineOpen.fromSpecStalk, Scheme.Hom.comp_app,
    hV.fromSpec_app_of_le _ hVU, ← X.presheaf.germ_res (homOfLE hVU) x hxV]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
have obtain : ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens) (hyU : y ∈ (↑U : Set ↥X)),
  Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hyU, -⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ y) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ (↑U : Set ↥X)
hxU : x ∈ U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
have rw : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = X.fromSpecStalk x
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ (↑U : Set ↥X)
hxU : x ∈ U
rw : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = X.fromSpecStalk x
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
have rw₁ : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = IsAffineOpen.fromSpecStalk hU hxU
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ (↑U : Set ↥X)
hxU : x ∈ U
rw : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = X.fromSpecStalk x
rw₁ : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = IsAffineOpen.fromSpecStalk hU hxU
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
have rw₂ : Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU =
  IsAffineOpen.fromSpecStalk hU hxU
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ (↑U : Set ↥X)
hxU : x ∈ U
rw : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = X.fromSpecStalk x
rw₁ : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = IsAffineOpen.fromSpecStalk hU hxU
rw₂ :
  Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hU hxU
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
have rw₃ : Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
  (Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU)
  (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ (↑U : Set ↥X)
hxU : x ∈ U
rw : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = X.fromSpecStalk x
rw₁ : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = IsAffineOpen.fromSpecStalk hU hxU
rw₂ :
  Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hU hxU
rw₃ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    (Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
have rw₄ : Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
  ((Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU)) ≫ IsAffineOpen.fromSpec hU)
  (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ (↑U : Set ↥X)
hxU : x ∈ U
rw : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = X.fromSpecStalk x
rw₁ : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = IsAffineOpen.fromSpecStalk hU hxU
rw₂ :
  Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hU hxU
rw₃ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    (Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
rw₄ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    ((Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU)) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
have rw₅ : Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
  (Spec.map (X.presheaf.germ U y hyU ≫ X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpec hU)
  (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hyU : y ∈ (↑U : Set ↥X)
hxU : x ∈ U
rw : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = X.fromSpecStalk x
rw₁ : Spec.map (X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpecStalk hU hyU = IsAffineOpen.fromSpecStalk hU hxU
rw₂ :
  Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hU hxU
rw₃ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    (Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
rw₄ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    ((Spec.map (X.presheaf.stalkSpecializes h) ≫ Spec.map (X.presheaf.germ U y hyU)) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
rw₅ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X)
    (Spec.map (X.presheaf.germ U y hyU ≫ X.presheaf.stalkSpecializes h) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
have rw₆ : Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x sorry) ≫ IsAffineOpen.fromSpec hU)
  (Spec.map (X.presheaf.germ U x hxU) ≫ IsAffineOpen.fromSpec hU)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
    TopCat.Presheaf.germ_stalkSpecializes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have obtain : ∀ (U : TopologicalSpace.Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)),
  Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := Y.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ (f x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have obtain : ∀ (V : TopologicalSpace.Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X))
  (hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier), Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
Tactic: obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    hxU (f ⁻¹ᵁ U).2