awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ ∃ (U : X.Opens) (V : Y.Opens),
    U = ⊤ ∧
      V = Scheme.Hom.opensRange f ∧
        ((∀ [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))) →
          ∀ [hX : IsReduced Y] (s : (↑Γ(Y, V) : Type u_1)) (hs : Y.basicOpen s = ⊥) (x : ↥Y) (hx : x ∈ V),
            Eq (α := (↑(Y.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 := Y.sheaf.presheaf.stalk x) (Y.sheaf.presheaf.germ V x hx) :
                    (a : (↑(Y.sheaf.presheaf.obj (op V)) : Type u_1)) → (↑(Y.sheaf.presheaf.stalk x) : Type u_1))
                  s :
                (↑(Y.sheaf.presheaf.stalk x) : Type u_1))
              (0 : (↑(Y.sheaf.presheaf.stalk x) : Type u_1)))
have h : (∀ [hX : IsReduced X] (s : (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X)
    (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
    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 (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : 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 Y] (s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)) (hs : Y.basicOpen s = ⊥) (x : ↥Y)
    (hx : x ∈ Scheme.Hom.opensRange f),
    Eq (α := (↑(Y.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 := Y.sheaf.presheaf.stalk x)
              (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) x hx) :
            (a : (↑(Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) : Type u_1)) →
              (↑(Y.sheaf.presheaf.stalk x) : Type u_1))
          s :
        (↑(Y.sheaf.presheaf.stalk x) : Type u_1))
      (0 : (↑(Y.sheaf.presheaf.stalk x) : Type u_1))
Tactic: refine ⟨f ⁻¹ᵁ f.opensRange, f.opensRange, by simp, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X)
    (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
    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 (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : 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 Y
s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)
hs : Y.basicOpen s = ⊥
x : ↥X
⊢ 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))
have this : IsReduced X
Tactic: haveI := isReduced_of_isOpenImmersion f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X)
    (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
    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 (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : 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 Y
s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ 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))
have h : X.basicOpen (U := f ⁻¹ᵁ Scheme.Hom.opensRange f)
    ((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) =
  ⊥
Tactic: specialize H (f.app _ s) _ x ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X)
    (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
    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 (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : 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 Y
s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ X.basicOpen (U := f ⁻¹ᵁ Scheme.Hom.opensRange f)
      ((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) =
    ⊥
have h : f ⁻¹ᵁ ⊥ = ⊥
Tactic: rw [← Scheme.preimage_basicOpen, hs]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X)
    (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
    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 (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : 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 Y
s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
⊢ f ⁻¹ᵁ ⊥ = ⊥
have h : (↑(f ⁻¹ᵁ ⊥) : Set ↥X) = (↑⊥ : Set ↥X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
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 :
  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))
⊢ 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))
have H₁ : Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
  ((CommRingCat.Hom.hom (X.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x sorry) :
        (a : (↑(X.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : 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 := Γ(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.presheaf.stalk x) : Type u_1))
  (0 : (↑(X.presheaf.stalk x) : Type u_1))
Tactic: have H : (X.presheaf.germ _ x _).hom _ = 0 := H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
⊢ 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))
have 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))
Tactic: rw [basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff] at hs
Cleared hypotheses: hs, x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
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 (α := (↑(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))
have 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))
Tactic: replace hs := (hs.map (Scheme.ΓSpecIso R).inv.hom).eq_zero
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (hypothesis)
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))
⊢ 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))
have hs₁ : s = 0
Tactic: rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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
⊢ 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))
have 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))
Tactic: rw [hs, map_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
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))
⊢ 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))
have h₁ : Eq.{u_1 + 1} (α := (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1)) 0 0
Tactic: rw [hs, map_zero]
-- 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))
    (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))
have h : ∀ (X : Scheme.{u_1}) (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))
Tactic: induction U using reduce_to_affine_global generalizing hX with
  | h₁ X U H =>
    obtain ⟨V, hx, i, H⟩ := H ⟨x, hx⟩
    specialize H (X.presheaf.map i.op s)
    rw [Scheme.basicOpen_res, hs] at H
    specialize H (inf_bot_eq _) x hx
    rw [← X.sheaf.presheaf.germ_res_apply i x hx s]
    exact H
  | h₂ X Y f =>
    refine ⟨f ⁻¹ᵁ f.opensRange, f.opensRange, by simp, rfl, ?_⟩
    rintro H hX s hs _ ⟨x, rfl⟩
    haveI := isReduced_of_isOpenImmersion f
    specialize H (f.app _ s) _ x ⟨x, rfl⟩
    · rw [← Scheme.preimage_basicOpen, hs]; ext1; simp [Opens.map]
    · have H : (X.presheaf.germ _ x _).hom _ = 0 := H
      rw [← Scheme.Hom.germ_stalkMap_apply f ⟨_, _⟩ x] at H
      apply_fun inv <| f.stalkMap x at H
      rw [← CommRingCat.comp_apply, CategoryTheory.IsIso.hom_inv_id, map_zero] at H
      exact H
  | h₃ R =>
    rw [basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff] at hs
    replace hs := (hs.map (Scheme.ΓSpecIso R).inv.hom).eq_zero
    rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply] at hs
    rw [hs, map_zero]
Cleared hypotheses: hX, U, s, hs, x, hx