awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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))
⊢ 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.germ V x hxV) :
        (a : (↑(X.presheaf.obj (op V)) : Type u_1)) → (↑(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) (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)) :
    (↑(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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsReduced Y
⊢ IsReduced X
have component_reduced : autoParam (∀ (U : X.Opens), _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)) IsReduced.component_reduced._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : IsReduced Y
U : X.Opens
⊢ _root_.IsReduced.{u_1} (↑Γ(X, U) : Type u_1)
have component_reduced : _root_.IsReduced.{u_1} (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u_1)
Tactic: rw [← f.preimage_image_eq U]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
R : CommRingCat
H : _root_.IsReduced.{u} (↑R : Type u)
⊢ IsReduced.{u} (Spec R)
have inst : ∀ (x : ↥(Spec R)), _root_.IsReduced.{u} (↑((Spec R).presheaf.stalk x) : Type u)
Tactic: apply +allowSynthFailures isReduced_of_isReduced_stalk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
R : CommRingCat
H : _root_.IsReduced.{u} (↑R : Type u)
x : ↥(Spec R)
⊢ _root_.IsReduced.{u} (↑((Spec R).presheaf.stalk x) : Type u)
have this : _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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
R : CommRingCat
⊢ IsReduced.{u_1} (Spec R) ↔ _root_.IsReduced.{u_1} (↑R : Type u_1)
have refine : IsReduced.{u_1} (Spec R) → _root_.IsReduced.{u_1} (↑R : Type u_1)
Tactic: refine ⟨?_, fun h => inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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)
have obtain : ∀ (i : 𝒰.I₀) (x : ↥(𝒰.X i)), _root_.IsReduced.{u_2} (↑(X.presheaf.stalk ((𝒰.f i) x)) : Type u_2)
Tactic: obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
inst : ∀ (i : 𝒰.I₀), IsReduced.{u_2} (𝒰.X i)
⊢ IsReduced X
have this : ∀ (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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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) ⊤
⊢ P U
have a : ∀ (x : ↥U), ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V
Tactic: apply h₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
⊢ ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U), P V
have 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
Tactic: obtain ⟨_, ⟨j, rfl⟩, hx, i⟩ :=
    X.affineBasisCover_is_basis.exists_subset_of_mem_open (SetLike.mem_coe.2 x.prop) U.isOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
have a : P U'
Tactic: refine ⟨U', hx, i', ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
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 U'
have h₂' : P (X := X.affineBasisCover.X j) ⊤ → P (Scheme.Hom.opensRange (X.affineBasisCover.f j))
Tactic: obtain ⟨_, _, rfl, rfl, h₂'⟩ := h₂ _ _ (X.affineBasisCover.f j)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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 U'
have a : P (X := X.affineBasisCover.X j) ⊤
Tactic: apply h₂'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
⊢ P X x
have 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
Tactic: obtain ⟨y, e⟩ := X.affineCover.covers x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
have h : x = (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y
Tactic: convert! h₂ (X.affineCover.f (X.affineCover.idx x)) y _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
⊢ P X x
have convert! : P (X.affineCover.X (Scheme.Cover.idx X.affineCover x)) y
Tactic: convert! h₂ (X.affineCover.f (X.affineCover.idx x)) y _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
⊢ x = (X.affineCover.f (Scheme.Cover.idx X.affineCover x)) y
have h : x = x
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
hX : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : X.basicOpen s = ⊥
⊢ s = 0
have 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))
Tactic: apply TopCat.Presheaf.section_ext X.sheaf U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
hX : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : X.basicOpen 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 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))
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
⊢ 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 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))
Tactic: obtain ⟨V, hx, i, H⟩ := H ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
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 :
  ∀ (hs : V ⊓ ⊥ = ⊥) (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))
⊢ 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_1) :
          (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 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 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 (inf_bot_eq _) x hx
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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 :
  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))
⊢ 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_1) :
          (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 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 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.sheaf.presheaf.map i.op) :
            (a : (↑(X.sheaf.presheaf.obj (op U)) : Type u_1)) → (↑(X.sheaf.presheaf.obj (op V)) : Type u_1))
          s :
        (↑(X.sheaf.presheaf.obj (op V)) : Type u_1)) :
    (↑(X.sheaf.presheaf.stalk x) : Type u_1))
  (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))
Tactic: rw [← X.sheaf.presheaf.germ_res_apply i x hx s]