awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Properties
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
change :
  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))
⊢ 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:
change (X.sheaf.presheaf.germ U x hx) s = (X.sheaf.presheaf.germ U x hx) 0

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.sheaf, TopCat.Presheaf.germ, TopCat.Sheaf.presheaf, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Properties
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
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))
⊢ 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:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.AlgebraicGeometry.Properties
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
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))
⊢ 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:
change X.presheaf.germ U x hx s = 0

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
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.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:
(hs.map _).eq_zero

Premises used: IsNilpotent.map, IsNilpotent.eq_zero
-- Module: Mathlib.AlgebraicGeometry.Properties
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.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:
exact (hs.map _).eq_zero

Premises used: IsNilpotent.map, IsNilpotent.eq_zero
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
eq_zero : ∀ (x_1 : (↑(X.presheaf.stalk x) : Type u_1)), IsNilpotent x_1 → x_1 = 0
⊢ _root_.IsReduced.{u_1} (↑(X.presheaf.stalk x) : Type u_1)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
g : (↑(X.presheaf.stalk x) : Type u_1)
n : ℕ
e : g ^ n = 0
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))
⊢ g = 0

Tactic:
obtain ⟨U, hxU, s, (rfl : (X.presheaf.germ U x hxU) s = g)⟩ := X.presheaf.exists_germ_eq g

Premises used: TopCat.Presheaf.exists_germ_eq, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, rfl, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
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 ^ 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

Premises used: CommRingCat.Hom.hom, map_zero, map_pow, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
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_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))
⊢ 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

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, TopCat.Presheaf.germ_eq, OfNat.ofNat, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Properties
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))
⊢ 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'

Premises used: map_zero, map_pow
-- Module: Mathlib.AlgebraicGeometry.Properties
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, 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))
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsReduced Y
component_reduced :
  autoParam (∀ (U : X.Opens), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)) IsReduced.component_reduced._autoParam
⊢ IsReduced X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsReduced Y
U : X.Opens
component_reduced : _root_.IsReduced.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)

Tactic:
rw [← f.preimage_image_eq U]

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsReduced Y
U : X.Opens
⊢ _root_.IsReduced.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)

Tactic:
isReduced_of_injective (inv <| f.app (f ''ᵁ U)).hom
    (asIso <| f.app (f ''ᵁ U) : Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.injective

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CategoryTheory.Iso.commRingCatIsoToRingEquiv, isReduced_of_injective, CommRingCat.Hom.hom, RingEquiv.injective, AlgebraicGeometry.Scheme.Hom.app, CategoryTheory.Iso.symm, CategoryTheory.inv, CategoryTheory.Functor.obj, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsReduced Y
U : X.Opens
⊢ _root_.IsReduced.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)

Tactic:
exact isReduced_of_injective (inv <| f.app (f ''ᵁ U)).hom
    (asIso <| f.app (f ''ᵁ U) : Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.injective

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CategoryTheory.Iso.commRingCatIsoToRingEquiv, isReduced_of_injective, CommRingCat.Hom.hom, RingEquiv.injective, AlgebraicGeometry.Scheme.Hom.app, CategoryTheory.Iso.symm, CategoryTheory.inv, CategoryTheory.Functor.obj, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 : Scheme
X : Scheme
U : X.Opens
inst : IsReduced X
⊢ IsReduced.{u_1} (↑U : Scheme)

Tactic:
isReduced_of_isOpenImmersion U.ι

Premises used: AlgebraicGeometry.isReduced_of_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
H : _root_.IsReduced.{u} (↑R : Type u)
inst : ∀ (x : ↥(Spec R)), _root_.IsReduced.{u} (↑((Spec R).presheaf.stalk x) : Type u)
⊢ IsReduced.{u} (Spec R)

Tactic:
apply +allowSynthFailures isReduced_of_isReduced_stalk

Premises used: AlgebraicGeometry.isReduced_of_isReduced_stalk
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
H : _root_.IsReduced.{u} (↑R : Type u)
x : ↥(Spec R)
⊢ _root_.IsReduced.{u} (Localization.AtPrime x.asIdeal)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
H : _root_.IsReduced.{u} (↑R : Type u)
x : ↥(Spec R)
⊢ _root_.IsReduced.{u} (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u)

Tactic:
have : _root_.IsReduced (CommRingCat.of <| Localization.AtPrime (PrimeSpectrum.asIdeal x)) := by
    dsimp; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
H : _root_.IsReduced.{u} (↑R : Type u)
x : ↥(Spec R)
this : _root_.IsReduced.{u} (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u)
⊢ _root_.IsReduced.{u} (↑((Spec R).presheaf.stalk x) : Type u)

Tactic:
isReduced_of_injective (Spec.stalkIso R x).hom.hom
    (Spec.stalkIso R x).commRingCatIsoToRingEquiv.injective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, isReduced_of_injective, CommRingCat.Hom.hom, RingEquiv.injective, AlgebraicGeometry.Spec.stalkIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
H : _root_.IsReduced.{u} (↑R : Type u)
x : ↥(Spec R)
this : _root_.IsReduced.{u} (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u)
⊢ _root_.IsReduced.{u} (↑((Spec R).presheaf.stalk x) : Type u)

Tactic:
exact isReduced_of_injective (Spec.stalkIso R x).hom.hom
    (Spec.stalkIso R x).commRingCatIsoToRingEquiv.injective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, isReduced_of_injective, CommRingCat.Hom.hom, RingEquiv.injective, AlgebraicGeometry.Spec.stalkIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
R : CommRingCat
⊢ IsReduced.{u_1} (Spec R) ↔ _root_.IsReduced.{u_1} (↑R : Type u_1)

Tactic:
⟨?_, fun h => inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
R : CommRingCat
refine : IsReduced.{u_1} (Spec R) → _root_.IsReduced.{u_1} (↑R : Type u_1)
⊢ IsReduced.{u_1} (Spec R) ↔ _root_.IsReduced.{u_1} (↑R : Type u_1)

Tactic:
refine ⟨?_, fun h => inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
R : CommRingCat
h : IsReduced.{u_1} (Spec R)
⊢ _root_.IsReduced.{u_1} (↑R : Type u_1)

Tactic:
isReduced_of_injective (Scheme.ΓSpecIso R).inv.hom
    (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv.injective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, isReduced_of_injective, CommRingCat.Hom.hom, RingEquiv.injective, AlgebraicGeometry.Scheme.ΓSpecIso, CategoryTheory.Iso.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
R : CommRingCat
h : IsReduced.{u_1} (Spec R)
⊢ _root_.IsReduced.{u_1} (↑R : Type u_1)

Tactic:
exact isReduced_of_injective (Scheme.ΓSpecIso R).inv.hom
    (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv.injective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, isReduced_of_injective, CommRingCat.Hom.hom, RingEquiv.injective, AlgebraicGeometry.Scheme.ΓSpecIso, CategoryTheory.Iso.symm, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsAffine X
inst_1 : _root_.IsReduced.{u_1} (↑Γ(X, ⊤) : Type u_1)
⊢ IsReduced X

Tactic:
isReduced_of_isOpenImmersion X.isoSpec.hom

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.isReduced_of_isOpenImmersion, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
inst : ∀ (i : 𝒰.I₀), IsReduced.{u_2} (𝒰.X i)
x : ↥X
obtain : ∀ (i : 𝒰.I₀) (x : ↥(𝒰.X i)), _root_.IsReduced.{u_2} (↑(X.presheaf.stalk ((𝒰.f i) x)) : Type u_2)
⊢ _root_.IsReduced.{u_2} (↑(X.presheaf.stalk x) : Type u_2)

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
inst : ∀ (i : 𝒰.I₀), IsReduced.{u_2} (𝒰.X i)
i : 𝒰.I₀
x : ↥(𝒰.X i)
⊢ _root_.IsReduced.{u_2} (↑(X.presheaf.stalk ((𝒰.f i) x)) : Type u_2)

Tactic:
isReduced_of_injective _
      (asIso <| (𝒰.f i).stalkMap x).commRingCatIsoToRingEquiv.injective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, isReduced_of_injective, CategoryTheory.PreZeroHypercover.f, RingEquiv.injective, AlgebraicGeometry.Scheme.Hom.stalkMap, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.asIso