awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
have rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₂ : Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
  IsAffineOpen.fromSpecStalk hV hxV ≫ f
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₃ : Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
  IsAffineOpen.fromSpecStalk hV hxV ≫ f
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₃ :
  Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₄ : Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU =
  IsAffineOpen.fromSpecStalk hV hxV ≫ f
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₃ :
  Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₄ :
  Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₅ : Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
  (Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU)
  ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₃ :
  Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₄ :
  Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₅ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₆ : Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
  (Spec.map (X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
  ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₃ :
  Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₄ :
  Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₅ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₆ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₇ : Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
  (Spec.map (X.presheaf.map (homOfLE hVU).op ≫ X.presheaf.germ V x hxV) ≫
    Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
  ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₃ :
  Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₄ :
  Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₅ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₆ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₇ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.map (homOfLE hVU).op ≫ X.presheaf.germ V x hxV) ≫
      Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₈ : Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
  (Spec.map (X.presheaf.germ V x hxV) ≫
    Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
  ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₃ :
  Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₄ :
  Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₅ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₆ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₇ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.map (homOfLE hVU).op ≫ X.presheaf.germ V x hxV) ≫
      Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₈ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₉ : Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
  (Spec.map (X.presheaf.germ V x hxV) ≫
    Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
  (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- 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)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (f ⁻¹ᵁ U).carrier
rw : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = X.fromSpecStalk x ≫ f
rw₁ : Spec.map (Hom.stalkMap f x) ≫ IsAffineOpen.fromSpecStalk hU hxU = IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₂ :
  Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₃ :
  Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₄ :
  Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
rw₅ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (Hom.app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₆ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ (f ⁻¹ᵁ U) x hxU) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₇ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.map (homOfLE hVU).op ≫ X.presheaf.germ V x hxV) ≫
      Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₈ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    ((Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV) ≫ f)
rw₉ :
  Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
    (Spec.map (X.presheaf.germ V x hxV) ≫
      Spec.map (X.presheaf.map (homOfLE hVU).op) ≫ Spec.map (Hom.app f U) ≫ IsAffineOpen.fromSpec hU)
    (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
⊢ Spec.map (Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) = X.fromSpecStalk x ≫ f
have rw₁₀ : Eq (α := Spec (X.presheaf.stalk x) ⟶ Y)
  (Spec.map (X.presheaf.germ V x hxV) ≫
    Spec.map (Hom.app f U ≫ X.presheaf.map (homOfLE hVU).op) ≫ IsAffineOpen.fromSpec hU)
  (Spec.map (X.presheaf.germ V x hxV) ≫ IsAffineOpen.fromSpec hV ≫ f)
Tactic: rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV,
    IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.Hom.germ_stalkMap f _ x hxU,
    IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV,
    Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _),
      Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.SpecMap_appLE_fromSpec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x : ↥X
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) {y : ↥X | y ⤳ x}
have 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
Tactic: ext y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
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
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y ↔
    Membership.mem (γ := Set ↥X) {y : ↥X | y ⤳ x} y
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (hypothesis)
Goal:
X : Scheme
x y : ↥X
hy : y ⤳ x
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y
have this : (X.fromSpecStalk y) (closedPoint (↑(X.presheaf.stalk y) : Type u)) = y
Tactic: have := fromSpecStalk_closedPoint (x := y)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (hypothesis)
Goal:
X : Scheme
x y : ↥X
hy : y ⤳ x
this : (X.fromSpecStalk y) (closedPoint (↑(X.presheaf.stalk y) : Type u)) = y
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec (X.presheaf.stalk x))) ⇑(X.fromSpecStalk x)) y
have this₁ : (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ U.fromSpecStalkOfMem x hxU ≫ U.ι = X.fromSpecStalk x
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [Opens.fromSpecStalkOfMem, Spec.map_inv, Category.assoc, IsIso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
x : ↥X
⊢ X.fromSpecStalk x ≫ X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial)
have 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 sorry))) ≫
      Iso.hom (ΓSpecIso (X.presheaf.stalk x))))
  (Spec.map (X.presheaf.germ ⊤ x trivial))
Tactic: rw [Scheme.toSpecΓ_naturality, ← SpecMap_ΓSpecIso_hom, ← Spec.map_comp,
    Scheme.fromSpecStalk_appTop]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ U.fromSpecStalkOfMem x hxU ≫ U.toSpecΓ = Spec.map (X.presheaf.germ U x hxU)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [fromSpecStalkOfMem, Opens.toSpecΓ, Category.assoc, fromSpecStalk_toSpecΓ_assoc,
    ← Spec.map_comp, ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Stalk (goal)
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)
have e_f : Eq (α := Γ(X, U) ⟶ X.presheaf.stalk x)
  (CategoryStruct.comp (Y := (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
      (U.topIso.inv ≫ (↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
      (inv (Hom.stalkMap U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))) :
    Γ(X, U) ⟶ X.presheaf.stalk x)
  (X.presheaf.germ U x hxU : X.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
Tactic: congr 1