awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
inst : ∀ (i : 𝒰.I₀), IsReduced.{u_2} (𝒰.X i)
⊢ ∀ (x : ↥X), _root_.IsReduced.{u_2} (↑(X.presheaf.stalk x) : Type u_2)

Tactic:
have (x : X) : _root_.IsReduced (X.presheaf.stalk x) := by
    obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
    exact isReduced_of_injective _
      (asIso <| (𝒰.f i).stalkMap x).commRingCatIsoToRingEquiv.injective
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
inst : ∀ (i : 𝒰.I₀), IsReduced.{u_2} (𝒰.X i)
this : ∀ (x : ↥X), _root_.IsReduced.{u_2} (↑(X.presheaf.stalk x) : Type u_2)
⊢ IsReduced X

Tactic:
isReduced_of_isReduced_stalk _

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

Tactic:
exact isReduced_of_isReduced_stalk _

Premises used: AlgebraicGeometry.isReduced_of_isReduced_stalk
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : {X : Scheme.{u_1}} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme.{u_1}) (U : X.Opens), (∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V) → P U
h₂ :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) [inst : IsOpenImmersion f],
    ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat.{u_1}), P (X := Spec R) ⊤
a : ∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V
⊢ P U

Tactic:
apply h₁
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : {X : Scheme.{u_1}} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme.{u_1}) (U : X.Opens), (∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V) → P U
h₂ :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) [inst : IsOpenImmersion f],
    ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat.{u_1}), P (X := Spec R) ⊤
x : ↥U
a :
  ∀ (j : X.affineBasisCover.I₀)
    (hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j)) (↑x : ↥X))
    (i : Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j) ⊆ (↑U : Set ↥X)),
    ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V
⊢ ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V

Tactic:
obtain ⟨_, ⟨j, rfl⟩, hx, i⟩ :=
    X.affineBasisCover_is_basis.exists_subset_of_mem_open (SetLike.mem_coe.2 x.prop) U.isOpen

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.affineBasisCover_is_basis, TopologicalSpace.Opens.isOpen, SetLike.mem_coe, Subtype.prop, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : {X : Scheme.{u_1}} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme.{u_1}) (U : X.Opens), (∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V) → P U
h₂ :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) [inst : IsOpenImmersion f],
    ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat.{u_1}), P (X := Spec R) ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j)) (↑x : ↥X)
i : Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j) ⊆ (↑U : Set ↥X)
U' : Opens ↥X := { carrier := Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
⊢ ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V

Tactic:
⟨U', hx, i', ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : {X : Scheme.{u_1}} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme.{u_1}) (U : X.Opens), (∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V) → P U
h₂ :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) [inst : IsOpenImmersion f],
    ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat.{u_1}), P (X := Spec R) ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j)) (↑x : ↥X)
i : Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j) ⊆ (↑U : Set ↥X)
U' : Opens ↥X := { carrier := Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
a : P U'
⊢ ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V

Tactic:
refine ⟨U', hx, i', ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : {X : Scheme.{u_1}} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme.{u_1}) (U : X.Opens), (∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V) → P U
h₂ :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) [inst : IsOpenImmersion f],
    ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat.{u_1}), P (X := Spec R) ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j)) (↑x : ↥X)
i : Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j) ⊆ (↑U : Set ↥X)
U' : Opens ↥X := { carrier := Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
⊢ P (X := X.affineBasisCover.X j) ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.f j))

Tactic:
obtain ⟨_, _, rfl, rfl, h₂'⟩ := h₂ _ _ (X.affineBasisCover.f j)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.affineBasisCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : {X : Scheme.{u_1}} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme.{u_1}) (U : X.Opens), (∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V) → P U
h₂ :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) [inst : IsOpenImmersion f],
    ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat.{u_1}), P (X := Spec R) ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j)) (↑x : ↥X)
i : Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j) ⊆ (↑U : Set ↥X)
U' : Opens ↥X := { carrier := Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
h₂' : P (X := X.affineBasisCover.X j) ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.f j))
a : P (X := X.affineBasisCover.X j) ⊤
⊢ P U'

Tactic:
apply h₂'
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : {X : Scheme.{u_1}} → X.Opens → Prop
X : Scheme
U : X.Opens
h₁ : ∀ (X : Scheme.{u_1}) (U : X.Opens), (∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V) → P U
h₂ :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) [inst : IsOpenImmersion f],
    ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)
h₃ : ∀ (R : CommRingCat.{u_1}), P (X := Spec R) ⊤
x : ↥U
j : X.affineBasisCover.I₀
hx : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j)) (↑x : ↥X)
i : Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j) ⊆ (↑U : Set ↥X)
U' : Opens ↥X := { carrier := Set.range (ι := ↥(X.affineBasisCover.X j)) ⇑(X.affineBasisCover.f j), is_open' := ⋯ }
i' : U' ⟶ U := homOfLE i
h₂' : P (X := X.affineBasisCover.X j) ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.f j))
⊢ P (X := X.affineBasisCover.X j) ⊤

Tactic:
apply h₃
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : (X : Scheme.{u_1}) → ↥X → Prop
h₁ : ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
obtain :
  ∀ (y : ↥(X.affineCover.X (Scheme.Cover.idx X.affineCover x)))
    (e : (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y = x), P X x
⊢ P X x

Tactic:
obtain ⟨y, e⟩ := X.affineCover.covers x

Premises used: AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : (X : Scheme.{u_1}) → ↥X → Prop
h₁ : ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
y : ↥(X.affineCover.X (Scheme.Cover.idx X.affineCover x))
e : (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y = x
⊢ P X ((X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y)

Tactic:
h₂ (X.affineCover.f (X.affineCover.idx x)) y _

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Cover.idx, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : (X : Scheme.{u_1}) → ↥X → Prop
h₁ : ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
y : ↥(X.affineCover.X (Scheme.Cover.idx X.affineCover x))
e : (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y = x
h : x = (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y
convert! : P (X.affineCover.X (Scheme.Cover.idx X.affineCover x)) y
⊢ P X x

Tactic:
convert! h₂ (X.affineCover.f (X.affineCover.idx x)) y _

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Cover.idx, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : (X : Scheme.{u_1}) → ↥X → Prop
h₁ : ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
y : ↥(X.affineCover.X (Scheme.Cover.idx X.affineCover x))
e : (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y = x
h h₃ : x = x
⊢ x = (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y

Tactic:
rw [e]
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
P : (X : Scheme.{u_1}) → ↥X → Prop
h₁ : ∀ (R : CommRingCat.{u_1}) (x : ↥(Spec R)), P (Spec R) x
h₂ : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)
X : Scheme
x : ↥X
y : ↥(X.affineCover.X (Scheme.Cover.idx X.affineCover x))
e : (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y = x
⊢ P (X.affineCover.X (Scheme.Cover.idx X.affineCover x)) y

Tactic:
apply h₁
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
hX : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : X.basicOpen s = ⊥
h :
  ∀ (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))
⊢ s = 0

Tactic:
apply TopCat.Presheaf.section_ext X.sheaf U

Premises used: AlgebraicGeometry.Scheme.sheaf, TopCat.Presheaf.section_ext
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
hX : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
h :
  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
hX : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
h :
  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_1 X : Scheme
U : X.Opens
H :
  ∀ (x : ↥U),
    ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U),
      ∀ [hX : IsReduced X] (s : (↑Γ(X, V) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X) (hx : x ∈ V),
        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 V x hx) :
                (a : (↑(X.sheaf.presheaf.obj (op V)) : 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))
hX : IsReduced X
s : (↑Γ(X, U) : Type u_1)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
h :
  ∀ (V : X.Opens) (hx_1 : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx) : ↥X) ∈ V) (i : V ⟶ U)
    (H :
      ∀ [hX : IsReduced X] (s : (↑Γ(X, V) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X) (hx : x ∈ V),
        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 V x hx) :
                (a : (↑(X.sheaf.presheaf.obj (op V)) : 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))
      (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))
    (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))

Tactic:
obtain ⟨V, hx, i, H⟩ := H ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 X : Scheme
U : X.Opens
H_1 :
  ∀ (x : ↥U),
    ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U),
      ∀ [hX : IsReduced X] (s : (↑Γ(X, V) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X) (hx : x ∈ V),
        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 V x hx) :
                (a : (↑(X.sheaf.presheaf.obj (op V)) : 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))
hX : IsReduced X
s : (↑Γ(X, U) : Type u_1)
hs : X.basicOpen s = ⊥
x : ↥X
hx_1 : x ∈ U
V : X.Opens
hx : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx_1) : ↥X) ∈ V
i : V ⟶ U
H :
  ∀ [hX : IsReduced X] (s : (↑Γ(X, V) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X) (hx : x ∈ V),
    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 V x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op V)) : 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))
⊢ ∀
    (hs :
      X.basicOpen (U := V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map i.op) :
              (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, V) : Type u_1))
            s) =
        ⊥)
    (x : ↥X) (hx : x ∈ V),
    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 V x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op V)) : 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.presheaf.map i.op) :
                (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, V) : Type u_1))
              s :
            (↑Γ(X, V) : Type u_1)) :
        (↑(X.sheaf.presheaf.stalk x) : Type u_1))
      (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))

Tactic:
specialize H (X.presheaf.map i.op s)

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace