awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IsReduced Y
s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
H_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) (X := X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) (Y :=
            X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯) :
          (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : Type u_1)) →
            (↑(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) (X := Γ(Y, Scheme.Hom.opensRange f)) (Scheme.Hom.app f (Scheme.Hom.opensRange f)) :
              (a : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1))
            s :
          (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) :
      (↑(X.sheaf.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))
H :
  Eq (α := (↑(Y.presheaf.stalk (f 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.presheaf.stalk (f x))) :
          (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(Y.presheaf.stalk (f 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 :=
                Y.presheaf.obj (op { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ })) (Y :=
                Y.presheaf.stalk (f x))
                (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯) :
              (a :
                  (↑(Y.presheaf.obj (op { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ })) : Type u_1)) →
                (↑(Y.presheaf.stalk (f x)) : Type u_1))
            s :
          (↑(Y.presheaf.stalk (f x)) : Type u_1)) :
      (↑(Y.presheaf.stalk (f x)) : Type u_1))
    (0 : (↑(Y.presheaf.stalk (f x)) : Type u_1))
⊢ Eq (α := (↑(Y.sheaf.presheaf.stalk (f 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 := Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) (Y :=
            Y.sheaf.presheaf.stalk (f x)) (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯) :
          (a : (↑(Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) : Type u_1)) →
            (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
        s :
      (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
    (0 : (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))

Tactic:
H

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange, setOf, Set.range
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IsReduced Y
s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
H_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) (X := X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) (Y :=
            X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯) :
          (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : Type u_1)) →
            (↑(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) (X := Γ(Y, Scheme.Hom.opensRange f)) (Scheme.Hom.app f (Scheme.Hom.opensRange f)) :
              (a : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1))
            s :
          (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) :
      (↑(X.sheaf.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))
H :
  Eq (α := (↑(Y.presheaf.stalk (f 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.presheaf.stalk (f x))) :
          (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(Y.presheaf.stalk (f 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 :=
                Y.presheaf.obj (op { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ })) (Y :=
                Y.presheaf.stalk (f x))
                (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯) :
              (a :
                  (↑(Y.presheaf.obj (op { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ })) : Type u_1)) →
                (↑(Y.presheaf.stalk (f x)) : Type u_1))
            s :
          (↑(Y.presheaf.stalk (f x)) : Type u_1)) :
      (↑(Y.presheaf.stalk (f x)) : Type u_1))
    (0 : (↑(Y.presheaf.stalk (f x)) : Type u_1))
⊢ Eq (α := (↑(Y.sheaf.presheaf.stalk (f 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 := Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) (Y :=
            Y.sheaf.presheaf.stalk (f x)) (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯) :
          (a : (↑(Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) : Type u_1)) →
            (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
        s :
      (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
    (0 : (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))

Tactic:
exact H
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
hX : IsReduced.{u_1} (Spec R)
s : (↑Γ(Spec R, ⊤) : Type u_1)
hs : (Spec R).basicOpen s = ⊥
x : ↥(Spec R)
hx : Membership.mem (γ := Opens ↥(Spec R)) ⊤ x
h :
  ∀
    (hs :
      IsNilpotent (R := (↑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))
            s :
          (↑R : Type u_1)))
    (x : ↥(Spec R)) (hx : Membership.mem (γ := Opens ↥(Spec R)) ⊤ x),
    Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) 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 := Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ) (Sheaf.presheaf (Spec R).sheaf) (op ⊤))
              (Y := Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x)
              (Presheaf.germ (Sheaf.presheaf (Spec R).sheaf) ⊤ x hx) :
            (a : (↑((Spec R).sheaf.presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).sheaf.presheaf.stalk x) : Type u_1))
          s :
        (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))
      (0 : (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))
⊢ Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) 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 := Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ) (Sheaf.presheaf (Spec R).sheaf) (op ⊤))
            (Y := Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x)
            (Presheaf.germ (Sheaf.presheaf (Spec R).sheaf) ⊤ x hx) :
          (a : (↑((Spec R).sheaf.presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).sheaf.presheaf.stalk x) : Type u_1))
        s :
      (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))
    (0 : (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))

Tactic:
rw [basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff] at hs

Premises used: AlgebraicGeometry.basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
hX : IsReduced.{u_1} (Spec R)
s : (↑Γ(Spec R, ⊤) : Type u_1)
hs :
  IsNilpotent (R := (↑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))
        s :
      (↑R : Type u_1))
x : ↥(Spec R)
hx : Membership.mem (γ := Opens ↥(Spec R)) ⊤ x
⊢ Eq (α := (↑Γ(Spec R, ⊤) : Type u_1))
    ((CommRingCat.Hom.hom (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))
          s) :
      (↑Γ(Spec R, ⊤) : Type u_1))
    (0 : (↑Γ(Spec R, ⊤) : Type u_1))

Tactic:
replace hs := (hs.map (Scheme.ΓSpecIso R).inv.hom).eq_zero
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
hX : IsReduced.{u_1} (Spec R)
s : (↑Γ(Spec R, ⊤) : Type u_1)
x : ↥(Spec R)
hx : Membership.mem (γ := Opens ↥(Spec R)) ⊤ x
hs :
  Eq (α := (↑Γ(Spec R, ⊤) : Type u_1))
    ((CommRingCat.Hom.hom (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))
          s) :
      (↑Γ(Spec R, ⊤) : Type u_1))
    (0 : (↑Γ(Spec R, ⊤) : Type u_1))
⊢ s = 0

Tactic:
rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply] at hs

Premises used: CommRingCat.id_apply, CategoryTheory.Iso.hom_inv_id, CommRingCat.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
hX : IsReduced.{u_1} (Spec R)
s : (↑Γ(Spec R, ⊤) : Type u_1)
x : ↥(Spec R)
hx : Membership.mem (γ := Opens ↥(Spec R)) ⊤ x
hs : s = 0
h :
  Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) 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 := Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ) (Sheaf.presheaf (Spec R).sheaf) (op ⊤))
            (Y := Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x)
            (Presheaf.germ (Sheaf.presheaf (Spec R).sheaf) ⊤ x hx) :
          (a : (↑((Spec R).sheaf.presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).sheaf.presheaf.stalk x) : Type u_1))
        0 :
      (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))
    (0 : (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))
h₁ h₂ : Eq.{u_1 + 1} (α := (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1)) 0 0
⊢ Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) 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 := Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ) (Sheaf.presheaf (Spec R).sheaf) (op ⊤))
            (Y := Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x)
            (Presheaf.germ (Sheaf.presheaf (Spec R).sheaf) ⊤ x hx) :
          (a : (↑((Spec R).sheaf.presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).sheaf.presheaf.stalk x) : Type u_1))
        s :
      (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))
    (0 : (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))

Tactic:
rw [hs, map_zero]

Premises used: map_zero
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
⊢ X.basicOpen s = ⊥ ↔ s = 0

Tactic:
⟨eq_zero_of_basicOpen_eq_bot s, ?_⟩

Premises used: AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
refine : s = 0 → X.basicOpen s = ⊥
⊢ X.basicOpen s = ⊥ ↔ s = 0

Tactic:
refine ⟨eq_zero_of_basicOpen_eq_bot s, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
U : X.Opens
⊢ X.basicOpen (U := U) 0 = ⊥

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
x : ↥X
hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x})
inst : IsReduced X
inr :
  ∀
    (this :
      ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
        [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1))
    (hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
wlog :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
⊢ IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)

Tactic:
wlog hX : ∃ R, X = Spec R
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
x : ↥X
hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x})
inst : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
inr :
  ∀ (i : X.affineCover.I₀) (x : ↥(X.affineCover.X i))
    (hx :
      Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
        (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))),
    IsField.{u_1} (↑(X.presheaf.stalk ((X.affineCover.f i) x)) : Type u_1)
⊢ IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)

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

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.Scheme.affineCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
⊢ IsReduced.{u_1} (X.affineCover.X i)

Tactic:
have inst : IsReduced (X.affineCover.X i) := isReduced_of_isOpenImmersion (X.affineCover.f i)
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst_1 : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
inst : IsReduced.{u_1} (X.affineCover.X i)
⊢ IsField.{u_1} (↑(X.presheaf.stalk ((X.affineCover.f i) x)) : Type u_1)

Tactic:
(asIso <| (X.affineCover.f i).stalkMap x).commRingCatIsoToRingEquiv.isField
      (this _ x ?_ ⟨_, rfl⟩)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.PreZeroHypercover.f, RingEquiv.toMulEquiv, MulEquiv.isField, Exists.intro, AlgebraicGeometry.Scheme.Hom.stalkMap, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst_1 : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
inst : IsReduced.{u_1} (X.affineCover.X i)
inr : Membership.mem (γ := Set (Set ↥(X.affineCover.X i))) (irreducibleComponents ↥(X.affineCover.X i)) (closure {x})
⊢ IsField.{u_1} (↑(X.presheaf.stalk ((X.affineCover.f i) x)) : Type u_1)

Tactic:
refine (asIso <| (X.affineCover.f i).stalkMap x).commRingCatIsoToRingEquiv.isField
      (this _ x ?_ ⟨_, rfl⟩)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.PreZeroHypercover.f, RingEquiv.toMulEquiv, MulEquiv.isField, Exists.intro, AlgebraicGeometry.Scheme.Hom.stalkMap, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst_1 : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
inst : IsReduced.{u_1} (X.affineCover.X i)
inr :
  Membership.mem (γ := Set (Set ↥(X.affineCover.X i))) (irreducibleComponents ↥(X.affineCover.X i))
    (Set.preimage (β := ↥X) (⇑(X.affineCover.f i)) (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X))))
⊢ Membership.mem (γ := Set (Set ↥(X.affineCover.X i))) (irreducibleComponents ↥(X.affineCover.X i)) (closure {x})

Tactic:
rw [(X.affineCover.f i).isOpenEmbedding.closure_eq_preimage_closure_image, Set.image_singleton]

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, Set.image_singleton, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Topology.IsEmbedding.closure_eq_preimage_closure_image
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst_1 : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
inst : IsReduced.{u_1} (X.affineCover.X i)
⊢ Membership.mem (γ := Set (Set ↥(X.affineCover.X i))) (irreducibleComponents ↥(X.affineCover.X i))
    (Set.preimage (β := ↥X) (⇑(X.affineCover.f i)) (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X))))

Tactic:
preimage_mem_irreducibleComponents hx (X.affineCover.f i).isOpenEmbedding
      ⟨X.affineCover.f i x, subset_closure rfl, _, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.ConcreteCategory.hom, subset_closure, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, preimage_mem_irreducibleComponents, And.intro, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
inst_1 : IsReduced X
this :
  ∀ (X : Scheme.{u_1}) (x : ↥X) (hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x}))
    [IsReduced X] (hX : ∃ (R : CommRingCat.{u_1}), X = Spec R), IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
hX : ¬∃ (R : CommRingCat.{u_1}), X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx :
  Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X)
    (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X)))
inst : IsReduced.{u_1} (X.affineCover.X i)
⊢ Membership.mem (γ := Set (Set ↥(X.affineCover.X i))) (irreducibleComponents ↥(X.affineCover.X i))
    (Set.preimage (β := ↥X) (⇑(X.affineCover.f i)) (closure (singleton (α := ↥X) ((X.affineCover.f i) x : ↥X))))

Tactic:
exact preimage_mem_irreducibleComponents hx (X.affineCover.f i).isOpenEmbedding
      ⟨X.affineCover.f i x, subset_closure rfl, _, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.ConcreteCategory.hom, subset_closure, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, preimage_mem_irreducibleComponents, And.intro, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.affineCover, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 X : Scheme
x : ↥X
hx : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {x})
inst : IsReduced X
hX : ∃ (R : CommRingCat.{u_1}), X = Spec R
obtain :
  ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R))
    (hx : Membership.mem (γ := Set (Set ↥(Spec R))) (irreducibleComponents ↥(Spec R)) (closure {x}))
    [IsReduced.{u_1} (Spec R)], IsField.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1)
⊢ IsField.{u_1} (↑(X.presheaf.stalk x) : Type u_1)

Tactic:
obtain ⟨R, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : Membership.mem (γ := Set (Set ↥(Spec R))) (irreducibleComponents ↥(Spec R)) (closure {x})
inst : IsReduced.{u_1} (Spec R)
rwa :
  Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) (PrimeSpectrum.vanishingIdeal {x})
rwa₁ rwa₂ rwa₃ rwa₄ :
  Membership.mem (γ := Set (Set (PrimeSpectrum (↑R : Type u_1))))
    (irreducibleComponents (PrimeSpectrum (↑R : Type u_1))) (closure {x})
⊢ Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) x.asIdeal

Tactic:
rwa [← PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes]

Premises used: PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : Membership.mem (γ := Set (Set ↥(Spec R))) (irreducibleComponents ↥(Spec R)) (closure {x})
inst : IsReduced.{u_1} (Spec R)
⊢ Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) x.asIdeal

Tactic:
replace hx : x.asIdeal ∈ minimalPrimes R := by
    rwa [← PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes]
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
inst : IsReduced.{u_1} (Spec R)
hx : Membership.mem (γ := Set (Ideal (↑R : Type u_1))) (minimalPrimes (↑R : Type u_1)) x.asIdeal
rw : Subsingleton.{u_1 + 1} (PrimeSpectrum (↑((Spec R).presheaf.stalk x) : Type u_1))
⊢ IsField.{u_1} (↑((Spec R).presheaf.stalk x) : Type u_1)

Tactic:
rw [← PrimeSpectrum.subsingleton_iff_isField_of_isReduced]

Premises used: PrimeSpectrum.subsingleton_iff_isField_of_isReduced