awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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_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 ⋯ ≫ Scheme.Hom.stalkMap sX x))
      (S.fromSpecStalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y)))
⊢ 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))

Tactic:
rw [← cancel_mono (S.fromSpecStalk _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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
⊢ 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 ⋯ ≫ Scheme.Hom.stalkMap sX x))
      (S.fromSpecStalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y)))

Tactic:
simpa only [Spec.map_comp, Category.assoc, Scheme.SpecMap_stalkMap_fromSpecStalk,
      Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc,
      Scheme.SpecMap_stalkSpecializes_fromSpecStalk]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
obtain :
  ∀ (U' : Opens ↥X) (h₁ : U' ∈ X.affineOpens) (h₂ : x ∈ U') (h₃ : U' ≤ U ⊓ V),
    hU.fromSpecStalk hxU = hV.fromSpecStalk hxV
⊢ 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⟩)

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd, And.intro, Iff.mp, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Stalk
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₂
transitivity₁ : fromSpecStalk h₁ h₂ = hV.fromSpecStalk hxV
⊢ hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

Tactic:
transitivity fromSpecStalk h₁ h₂

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
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)
rw₂ 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 ⋯) ≫ 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₁)

Tactic:
rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]

Premises used: AlgebraicGeometry.IsAffineOpen.map_fromSpec, Quiver.Hom.op, AlgebraicGeometry.Spec.map_comp_assoc, TopCat.Presheaf.germ_res, CategoryTheory.homOfLE, inf_le_left, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.Stalk
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)
rw₂ rw₃ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ V x ⋯) ≫ 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)

Tactic:
rw [← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op, ← Spec.map_comp_assoc,
      TopCat.Presheaf.germ_res]

Premises used: AlgebraicGeometry.IsAffineOpen.map_fromSpec, Quiver.Hom.op, inf_le_right, AlgebraicGeometry.Spec.map_comp_assoc, TopCat.Presheaf.germ_res, CategoryTheory.homOfLE, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥X
hxU : x ∈ U
⊢ hU.fromSpecStalk hxU = X.fromSpecStalk x

Tactic:
fromSpecStalk_eq ..

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq
-- Module: Mathlib.AlgebraicGeometry.Stalk
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))

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
-- Module: Mathlib.AlgebraicGeometry.Stalk
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
this : IsPreimmersion (X := Spec (X.presheaf.stalk x)) (Spec.map (X.presheaf.germ U x hx))
⊢ IsPreimmersion (X := Spec (X.presheaf.stalk x)) (Spec.map (X.presheaf.germ U x hx) ≫ hU.fromSpec)

Tactic:
apply IsPreimmersion.comp

Premises used: AlgebraicGeometry.IsPreimmersion.comp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
U V : X_1.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
X : Scheme
x : ↥X
⊢ IsPreimmersion (X.fromSpecStalk x)

Tactic:
IsAffineOpen.fromSpecStalk_isPreimmersion _ _ _

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpecStalk_isPreimmersion, AlgebraicGeometry.Scheme.fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
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
rw₁ rw₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) : ↥X) = 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

Tactic:
rw [← hU.primeIdealOf_eq_map_closedPoint ⟨x, hxU⟩, hU.fromSpec_primeIdealOf ⟨x, hxU⟩]

Premises used: Subtype.mk, AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
⊢ (X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) = x

Tactic:
IsAffineOpen.fromSpecStalk_closedPoint _ _

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
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 ⋯))
⊢ 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 ⋯))

Tactic:
obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    hxU U.2

Premises used: TopologicalSpace.Opens.is_open', AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.Scheme.Opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Stalk
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)
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 ⋯))) ≫
        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 ⋯)))
⊢ 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 ⋯))

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]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.IsAffineOpen.fromSpecStalk, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le, AlgebraicGeometry.Scheme.toLocallyRingedSpace, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
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)
⊢ 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 ⋯))) ≫
        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 ⋯)))

Tactic:
simp [Category.assoc, ← ΓSpecIso_inv_naturality_assoc]

Premises used: AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
⊢ Hom.appTop (X.fromSpecStalk x) =
    X.presheaf.germ ⊤ x trivial ≫
      Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ (Spec (X.presheaf.stalk x)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
fromSpecStalk_app ..

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, AlgebraicGeometry.Scheme.fromSpecStalk_app
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x y : ↥X
h : x ⤳ y
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
⊢ 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

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Stalk
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)
rw₆ rw₇ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ X) (Spec.map (X.presheaf.germ U x ⋯) ≫ 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

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]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.IsAffineOpen.fromSpecStalk, TopCat.Presheaf.germ_stalkSpecializes, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
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
⊢ 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

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Stalk
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)
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
⊢ 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

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', AlgebraicGeometry.Scheme.isBasis_affineOpens, CategoryTheory.Functor.obj, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
h :
  ∀ (y : ↥X),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y ↔
      Membership.mem (γ := Set ↥X) {y : ↥X | y ⤳ x} y
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) {y : ↥X | y ⤳ x}

Tactic:
ext y
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x y : ↥X
h :
  Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y →
    Membership.mem (γ := Set ↥X) {y : ↥X | y ⤳ x} y
h₁ :
  Membership.mem (γ := Set ↥X) {y : ↥X | y ⤳ x} y →
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y ↔
    Membership.mem (γ := Set ↥X) {y : ↥X | y ⤳ x} y

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
y : ↥(Spec (X.presheaf.stalk x))
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) {y : ↥X | y ⤳ x} ((X.fromSpecStalk x) y : ↥X)

Tactic:
((IsLocalRing.specializes_closedPoint y).map (X.fromSpecStalk x).continuous).trans
      (specializes_of_eq fromSpecStalk_closedPoint)

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, Specializes, Set.Mem, setOf, IsLocalRing.specializes_closedPoint, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.fromSpecStalk, Specializes.trans, Specializes.map, specializes_of_eq
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
y : ↥(Spec (X.presheaf.stalk x))
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) {y : ↥X | y ⤳ x} ((X.fromSpecStalk x) y : ↥X)

Tactic:
exact ((IsLocalRing.specializes_closedPoint y).map (X.fromSpecStalk x).continuous).trans
      (specializes_of_eq fromSpecStalk_closedPoint)

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, IsLocalRing.specializes_closedPoint, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.fromSpecStalk, Specializes.trans, Specializes.map, specializes_of_eq
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x y : ↥X
hy : y ⤳ x
⊢ (X.fromSpecStalk y) (closedPoint (↑(X.presheaf.stalk y) : Type u)) = y

Tactic:
have := fromSpecStalk_closedPoint (x := y)
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x y : ↥X
hy : y ⤳ x
this : (X.fromSpecStalk y) (closedPoint (↑(X.presheaf.stalk y) : Type u)) = y
⊢ (Spec.map (X.presheaf.stalkSpecializes hy) ≫ X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk y) : Type u)) = y

Tactic:
rw [← SpecMap_stalkSpecializes_fromSpecStalk hy] at this

Premises used: AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x y : ↥X
hy : y ⤳ x
this :
  (Spec.map (X.presheaf.stalkSpecializes hy) ≫ X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk y) : Type u)) = y
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y

Tactic:
⟨_, this⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x y : ↥X
hy : y ⤳ x
this :
  (Spec.map (X.presheaf.stalkSpecializes hy) ≫ X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk y) : Type u)) = y
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y

Tactic:
exact ⟨_, this⟩
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ U.fromSpecStalkOfMem x hxU ≫ U.ι = X.fromSpecStalk x

Tactic:
simp only [Opens.fromSpecStalkOfMem, Spec.map_inv, Category.assoc, IsIso.inv_comp_eq]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem, CategoryTheory.IsIso.inv_comp_eq, AlgebraicGeometry.Spec.map_inv
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
(Scheme.SpecMap_stalkMap_fromSpecStalk U.ι (x := ⟨x, hxU⟩)).symm

Premises used: AlgebraicGeometry.Scheme.Opens.ι, Eq.symm, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (Scheme.SpecMap_stalkMap_fromSpecStalk U.ι (x := ⟨x, hxU⟩)).symm

Premises used: AlgebraicGeometry.Scheme.Opens.ι, Eq.symm, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
rw :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Spec Γ(X, ⊤))
    (Spec.map
      ((X.presheaf.germ ⊤ x trivial ≫
          Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫
            (Spec (X.presheaf.stalk x)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) ≫
        Iso.hom (ΓSpecIso (X.presheaf.stalk x))))
    (Spec.map (X.presheaf.germ ⊤ x trivial))
⊢ X.fromSpecStalk x ≫ X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial)

Tactic:
rw [Scheme.toSpecΓ_naturality, ← SpecMap_ΓSpecIso_hom, ← Spec.map_comp,
    Scheme.fromSpecStalk_appTop]

Premises used: AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.fromSpecStalk_appTop, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
⊢ Eq (α := Spec (X.presheaf.stalk x) ⟶ Spec Γ(X, ⊤))
    (Spec.map
      ((X.presheaf.germ ⊤ x trivial ≫
          Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫
            (Spec (X.presheaf.stalk x)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) ≫
        Iso.hom (ΓSpecIso (X.presheaf.stalk x))))
    (Spec.map (X.presheaf.germ ⊤ x trivial))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ U.fromSpecStalkOfMem x hxU ≫ U.toSpecΓ = Spec.map (X.presheaf.germ U x hxU)

Tactic:
rw [fromSpecStalkOfMem, Opens.toSpecΓ, Category.assoc, fromSpecStalk_toSpecΓ_assoc,
    ← Spec.map_comp, ← Spec.map_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem, AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Scheme.Opens.toSpecΓ