awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
f : (↑R : Type u_1)
⊢ Eq.{u_1 + 1} (α := (Spec R).Opens)
    ((Spec R).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.ΓSpecIso R).inv :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
        f))
    (PrimeSpectrum.basicOpen f)
have h : ∀ (x : ↥(Spec R)),
  x ∈
      (↑((Spec R).basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Scheme.ΓSpecIso R).inv :
                (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
              f)) :
        Set ↥(Spec R)) ↔
    x ∈ (↑(PrimeSpectrum.basicOpen f) : Set ↥(Spec R))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
⊢ x ∈
      (↑((Spec R).basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Scheme.ΓSpecIso R).inv :
                (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
              f)) :
        Set ↥(Spec R)) ↔
    x ∈ (↑(PrimeSpectrum.basicOpen f) : Set ↥(Spec R))
have h : IsUnit (M := (↑((Spec R).presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := (Spec R).presheaf.obj (op ⊤)) (Y := (Spec R).presheaf.stalk x)
            ((Spec R).presheaf.germ ⊤ x _root_.trivial) :
          (a : (↑((Spec R).presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Scheme.ΓSpecIso R).inv :
              (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
            f :
          (↑Γ(Spec R, ⊤) : Type u_1)) :
      (↑((Spec R).presheaf.stalk x) : Type u_1)) ↔
  Membership.mem (γ := Opens ↥(Spec R)) (PrimeSpectrum.basicOpen f) x
Tactic: simp only [SetLike.mem_coe, Scheme.mem_basicOpen_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
⊢ IsUnit (M := (↑((Spec R).presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X := (Spec R).presheaf.obj (op ⊤)) (Y := (Spec R).presheaf.stalk x)
              ((Spec R).presheaf.germ ⊤ x _root_.trivial) :
            (a : (↑((Spec R).presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).presheaf.stalk x) : Type u_1))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Scheme.ΓSpecIso R).inv :
                (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
              f :
            (↑Γ(Spec R, ⊤) : Type u_1)) :
        (↑((Spec R).presheaf.stalk x) : Type u_1)) ↔
    Membership.mem (γ := Opens ↥(Spec R)) (PrimeSpectrum.basicOpen f) x
have h : IsUnit (M := (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1))
    ((algebraMap (↑R : Type u_1) (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1) :
          (a : (↑R : Type u_1)) → (↑((structurePresheafInCommRingCat (↑R : Type u_1)).stalk x) : Type u_1))
        f :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1)) ↔
  f ∉ x.asIdeal
Tactic: suffices IsUnit (algebraMap _ ((structurePresheafInCommRingCat ↑R).stalk x) f) ↔
    f ∉ PrimeSpectrum.asIdeal x by exact this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
⊢ IsUnit (M := (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1))
      ((algebraMap (↑R : Type u_1) (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1) :
            (a : (↑R : Type u_1)) → (↑((structurePresheafInCommRingCat (↑R : Type u_1)).stalk x) : Type u_1))
          f :
        (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1)) ↔
    f ∉ x.asIdeal
have h : IsUnit (M := Localization.AtPrime x.asIdeal)
    ((algebraMap (↑R : Type u_1) (Localization.AtPrime x.asIdeal) :
          (a : (↑R : Type u_1)) → Localization.AtPrime x.asIdeal)
        f :
      Localization.AtPrime x.asIdeal) ↔
  f ∉ x.asIdeal
Tactic: rw [← isUnit_map_iff (StructureSheaf.stalkIso R x).symm, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
f : (↑Γ(Spec R, ⊤) : Type u_1)
⊢ (Spec R).basicOpen f =
    PrimeSpectrum.basicOpen
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.ΓSpecIso R).hom :
          (a : (↑Γ(Spec R, ⊤) : Type u_1)) → (↑R : Type u_1))
        f)
have h : f =
  (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) (Scheme.ΓSpecIso R).inv :
      (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.ΓSpecIso R).hom :
        (a : (↑Γ(Spec R, ⊤) : Type u_1)) → (↑R : Type u_1))
      f)
Tactic: convert! basicOpen_eq_of_affine ((Scheme.ΓSpecIso R).hom f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Γ(Spec Γ(X, V), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom h))) ⁻¹ᵁ W)
have refl : ∀ (W : (Spec Γ(X, U)).Opens),
  Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) ⁻¹ᵁ W)
Tactic: cases h
Cleared hypotheses: V, h, W
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
have rw : Scheme.Spec.map (Quiver.Hom.op (𝟙 Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
Tactic: rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
rw : Scheme.Spec.map (Quiver.Hom.op (𝟙 Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
⊢ Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
have rw₁ : Scheme.Spec.map (𝟙 (op Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
Tactic: rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
rw : Scheme.Spec.map (Quiver.Hom.op (𝟙 Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
rw₁ : Scheme.Spec.map (𝟙 (op Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
⊢ Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
have rw₂ : 𝟙 (Scheme.Spec.obj (op Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
Tactic: rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (hypothesis)
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom h)))) W = eqToHom ⋯
have this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
Tactic: have : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 _ := by
    rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
⊢ Hom.app (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom h)))) W = eqToHom ⋯
have refl : ∀ (W : (Spec Γ(X, U)).Opens), Hom.app (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))) W = eqToHom sorry
Tactic: cases h
Cleared hypotheses: V, h, W
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) W = eqToHom ⋯
have refl : Hom.app (𝟙 (Scheme.Spec.obj (op Γ(X, U)))) W ≫ (Scheme.Spec.obj (op Γ(X, U))).presheaf.map (Quiver.Hom.op (eqToHom sorry)) =
  eqToHom sorry
Tactic: refine (Scheme.Hom.congr_app this _).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx : (↑x : ↥X) ∈ X.basicOpen s
n : ℕ
hf : s ^ n * f = 0
⊢ Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        f :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
have rw : ∀
  (hx :
    IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) sorry) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          s :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)))
  {n : ℕ} (hf : s ^ n * f = 0),
  Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) sorry) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        f :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
Tactic: rw [Scheme.mem_basicOpen X s x x.2] at hx
Cleared hypotheses: hx, n, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        (s ^ n) :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
have rw : IsUnit
  (HPow.hPow (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) sorry) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    n)
Tactic: rw [map_pow]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (hypothesis)
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
⊢ Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        f :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
have hu : IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) sorry) :
        (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      (s ^ n) :
    (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
Tactic: have hu : IsUnit (X.presheaf.germ _ x x.2 (s ^ n)) := by
    rw [map_pow]
    exact IsUnit.pow n hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
hu :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        (s ^ n) :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
⊢ Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        f :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
have rw : HMul.hMul (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) (β := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) sorry) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        (s ^ n) :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) sorry) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        f :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) =
  0
Tactic: rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
hu :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        (s ^ n) :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
rw :
  HMul.hMul (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) (β := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          (s ^ n) :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          f :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) =
    0
⊢ Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        f :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
have rw₁ : Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) sorry) :
        (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      (s ^ n * f) :
    (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
  (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
Tactic: rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x : ↥Y) = x
have change : Eq (α := ↥X) ((e.hom ≫ e.inv) x : ↥X)
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (PresheafedSpace.Hom.base (𝟙 X.toPresheafedSpace)) :
        (a : ↥X) → ↥X)
      x :
    ↥X)
Tactic: change (e.hom ≫ e.inv) x = 𝟙 X.toPresheafedSpace x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
e : X ≅ Y
y : ↥Y
⊢ e.hom (e.inv y : ↥X) = y
have change : Eq (α := ↥Y) ((e.inv ≫ e.hom) y : ↥Y)
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (PresheafedSpace.Hom.base (𝟙 Y.toPresheafedSpace)) :
        (a : ↥Y) → ↥Y)
      y :
    ↥Y)
Tactic: change (e.inv ≫ e.hom) y = 𝟙 Y.toPresheafedSpace y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
s : Set (↑R : Type u_1)
⊢ Eq (α := Set ↥(Spec R))
    ((Spec R).zeroLocus (U := ⊤)
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ''
        s))
    (PrimeSpectrum.zeroLocus s)
have h : ∀ (x : ↥(Spec R)),
  Membership.mem (γ := Set ↥(Spec R))
      ((Spec R).zeroLocus (U := ⊤)
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
            (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ''
          s))
      x ↔
    Membership.mem (γ := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
s : Set (↑R : Type u_1)
x : ↥(Spec R)
⊢ Membership.mem (γ := Set ↥(Spec R))
      ((Spec R).zeroLocus (U := ⊤)
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
            (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ''
          s))
      x ↔
    Membership.mem (γ := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus s) x
have h : (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔
  Membership.mem (γ := Set (PrimeSpectrum (↑R : Type u_1))) (PrimeSpectrum.zeroLocus s) x
Tactic: suffices (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s by simpa
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
s : Set (↑Γ(Spec R, ⊤) : Type u_1)
⊢ (Spec R).zeroLocus s =
    PrimeSpectrum.zeroLocus
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ⁻¹'
        s)
have h : s =
  Set.image (α := (↑R : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
      (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
    ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
        (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ⁻¹'
      s)
Tactic: convert! Spec_zeroLocus_eq_zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R : CommRingCat
s : Set (↑Γ(Spec R, ⊤) : Type u_1)
⊢ s =
    Set.image (α := (↑R : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
        (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ⁻¹'
        s)
have h : Function.Surjective (α := (↑R : Type u_1)) (β := (↑Γ(Spec R, ⊤) : Type u_1))
  (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
    (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
Tactic: rw [Set.image_preimage_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f y = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯
have rw : stalkMap f x ≫ X.presheaf.stalkSpecializes sorry = stalkMap f x ≫ X.presheaf.stalkSpecializes sorry
Tactic: rw [stalkSpecializes_stalkMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
rw : stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f y = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯
have h₁ : y ⤳ x
Tactic: rw [stalkSpecializes_stalkMap]