awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a ∈ s, a ∉ (↑p.asHomogeneousIdeal : Set A)
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U
have h_nhds : ∀ (f : A) (hfs : f ∈ s) (hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)),
  ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U
Tactic: obtain ⟨f, hfs, hfp⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)
⊢ ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U
have h_nhds : (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜)) ⊆ U
Tactic: refine ⟨basicOpen 𝒜 f, ⟨f, rfl⟩, hfp, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : f ∉ (↑p.asHomogeneousIdeal : Set A)
⊢ (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜)) ⊆ U
have h_nhds : Subset (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) (zeroLocus 𝒜 {f})
Tactic: rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x y : ProjectiveSpectrum 𝒜
⊢ x ≤ y ↔ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (closure {x}) y
have rw : x.asHomogeneousIdeal ≤ y.asHomogeneousIdeal ↔ (↑x.asHomogeneousIdeal : Set A) ⊆ (↑y.asHomogeneousIdeal : Set A)
Tactic: rw [← as_ideal_le_as_ideal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus,
    vanishingIdeal_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
⊢ QuasiSober.{u_1} ↥X
have hS : ∀
  (s :
    (↑(Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) : Type u_1)),
  IsOpen (↑s : Set ↥X)
Tactic: apply +allowSynthFailures
    quasiSober_of_open_cover (Set.range fun x => Set.range <| (X.affineCover.f x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
hS :
  ∀
    (s :
      (↑(Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) :
        Type u_1)),
    IsOpen (↑s : Set ↥X)
⊢ QuasiSober.{u_1} ↥X
have inst : ∀
  (s :
    (↑(Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) : Type u_1)),
  QuasiSober.{u_1} (↑(↑s : Set ↥X) : Type u_1)
Tactic: apply +allowSynthFailures
    quasiSober_of_open_cover (Set.range fun x => Set.range <| (X.affineCover.f x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
hS :
  ∀
    (s :
      (↑(Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) :
        Type u_1)),
    IsOpen (↑s : Set ↥X)
inst :
  ∀
    (s :
      (↑(Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) :
        Type u_1)),
    QuasiSober.{u_1} (↑(↑s : Set ↥X) : Type u_1)
⊢ QuasiSober.{u_1} ↥X
have hS' : Eq.{u_1 + 1} (α := Set ↥X)
  (⋃₀ Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) ⊤
Tactic: apply +allowSynthFailures
    quasiSober_of_open_cover (Set.range fun x => Set.range <| (X.affineCover.f x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
⊢ Eq.{u_1 + 1} (α := Set ↥X)
    (⋃₀ Set.range fun (x : X.affineCover.I₀) ↦ Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) ⊤
have hS' : ∀ (x : ↥X),
  Membership.mem (γ := Set ↥X) (⋃ (x : X.affineCover.I₀), Set.range (ι := ↥(X.affineCover.X x)) ⇑(X.affineCover.f x)) x
Tactic: rw [Set.top_eq_univ, Set.sUnion_range, Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : ∀ (x : ↥X), _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
⊢ IsReduced X
have refine : ∀ (U : X.Opens) (s : (↑Γ(X, U) : Type u_1)) (hs : IsNilpotent s), s = 0
Tactic: refine ⟨fun U => ⟨fun s hs => ?_⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : ∀ (x : ↥X), _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : IsNilpotent s
⊢ s = 0
have apply : ∀ (x : ↥X) (hx : x ∈ U),
  Eq (α := (↑(X.sheaf.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) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
          (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.sheaf.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) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
          (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.sheaf.presheaf.stalk x) : Type u_1))
Tactic: apply Presheaf.section_ext X.sheaf U s 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : ∀ (x : ↥X), _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : IsNilpotent s
x : ↥X
hx : x ∈ U
⊢ Eq (α := (↑(X.sheaf.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) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
          (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.sheaf.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) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
          (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.sheaf.presheaf.stalk x) : Type u_1))
have rw : Eq (α := (↑(X.sheaf.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) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
        (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.stalk x) : Type u_1))
      s :
    (↑(X.sheaf.presheaf.stalk x) : Type u_1))
  (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : ∀ (x : ↥X), _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : IsNilpotent s
x : ↥X
hx : x ∈ U
⊢ Eq (α := (↑(X.sheaf.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) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
          (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.sheaf.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))
have change : Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      s :
    (↑(X.presheaf.stalk x) : Type u_1))
  (0 : (↑(X.presheaf.stalk x) : Type u_1))
Tactic: change X.presheaf.germ U x hx s = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
⊢ _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
have eq_zero : ∀ (x_1 : (↑(X.presheaf.stalk x) : Type u_1)), IsNilpotent x_1 → x_1 = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
g : (↑(X.presheaf.stalk x) : Type u_1)
n : ℕ
e : g ^ n = 0
⊢ g = 0
have eq_zero : ∀ (U : Opens ↥X) (hxU : x ∈ U)
  (s :
    ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op U)))
  (e :
    HPow.hPow (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
            s :
          (↑(X.presheaf.stalk x) : Type u_1))
        n =
      0),
  Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
Tactic: obtain ⟨U, hxU, s, (rfl : (X.presheaf.germ U x hxU) s = g)⟩ := X.presheaf.exists_germ_eq g
Cleared hypotheses: g, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op U))
e :
  HPow.hPow (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          s :
        (↑(X.presheaf.stalk x) : Type u_1))
      n =
    0
⊢ Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
have e₁ : Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      (s ^ n) :
    (↑(X.presheaf.stalk x) : Type u_1))
  ((CommRingCat.Hom.hom (X.presheaf.germ U x hxU) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      0 :
    (↑(X.presheaf.stalk x) : Type u_1))
Tactic: rw [← map_pow, ← map_zero (X.presheaf.germ _ x hxU).hom] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op U))
e :
  Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        (s ^ n) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
⊢ Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
have eq_zero : ∀ (V : Opens ↥X) (hxV : x ∈ V) (iU iV : V ⟶ U)
  (e' :
    Eq (α := (↑(X.presheaf.obj (op V)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map iU.op) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
          (s ^ n) :
        (↑(X.presheaf.obj (op V)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map iV.op) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
          0 :
        (↑(X.presheaf.obj (op V)) : Type u_1))),
  Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
Tactic: obtain ⟨V, hxV, iU, iV, (e' : (X.presheaf.map iU.op) (s ^ n) = (X.presheaf.map iV.op) 0)⟩ :=
    X.presheaf.germ_eq x hxU hxU _ 0 e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op U))
e :
  Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        (s ^ n) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' :
  Eq (α := (↑(X.presheaf.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        (s ^ n) :
      (↑(X.presheaf.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iV.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        0 :
      (↑(X.presheaf.obj (op V)) : Type u_1))
⊢ Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
have e'₁ : HPow.hPow (α := (↑(X.presheaf.obj (op V)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        s :
      (↑(X.presheaf.obj (op V)) : Type u_1))
    n =
  0
Tactic: rw [map_pow, map_zero] at e'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op U))
e :
  Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        (s ^ n) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' :
  HPow.hPow (α := (↑(X.presheaf.obj (op V)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.map iU.op) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
          s :
        (↑(X.presheaf.obj (op V)) : Type u_1))
      n =
    0
⊢ Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
have e'₁ : Eq (α := (↑Γ(X, V) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X.presheaf.map iU.op) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
      s :
    (↑(X.presheaf.obj (op V)) : Type u_1))
  (0 : (↑Γ(X, V) : Type u_1))
Tactic: replace e' := (IsNilpotent.mk _ _ e').eq_zero (R := Γ(X, V))
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op U))
e :
  Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        (s ^ n) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' :
  Eq (α := (↑Γ(X, V) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        s :
      (↑(X.presheaf.obj (op V)) : Type u_1))
    (0 : (↑Γ(X, V) : Type u_1))
⊢ Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
have eq_zero : Eq (α := (↑(X.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) (Y := X.presheaf.stalk x) (X.presheaf.map iU.op ≫ X.presheaf.germ V x hxV) :
        (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      s :
    (↑(X.presheaf.stalk x) : Type u_1))
  (0 : (↑(X.presheaf.stalk x) : Type u_1))
Tactic: rw [← X.presheaf.germ_res iU x hxV, CommRingCat.comp_apply, e', map_zero]