awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀
    (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))
⊢ ∀ (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))

Tactic:
rw [Scheme.basicOpen_res, hs] at H

Premises used: AlgebraicGeometry.Scheme.basicOpen_res
-- 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 :
  ∀ (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 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

Premises used: inf_bot_eq
-- 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 :
  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))
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))
⊢ 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))

Tactic:
rw [← X.sheaf.presheaf.germ_res_apply i x hx s]

Premises used: TopCat.Presheaf.germ_res_apply, AlgebraicGeometry.Scheme.sheaf, TopCat.Sheaf.presheaf
-- 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 :
  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 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:
H

Premises used: Set.Mem
-- 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 :
  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 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:
exact H
-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange f = ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Properties
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 : ↥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))
⊢ ∃ (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)))

Tactic:
refine ⟨f ⁻¹ᵁ f.opensRange, f.opensRange, by simp, rfl, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Properties
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
⊢ IsReduced X

Tactic:
haveI := isReduced_of_isOpenImmersion f
-- Module: Mathlib.AlgebraicGeometry.Properties
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
h : f ⁻¹ᵁ ⊥ = ⊥
⊢ 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:
rw [← Scheme.preimage_basicOpen, hs]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Properties
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
h : (↑(f ⁻¹ᵁ ⊥) : Set ↥X) = (↑⊥ : Set ↥X)
⊢ f ⁻¹ᵁ ⊥ = ⊥

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Properties
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 ⁻¹ᵁ ⊥) : Set ↥X) = (↑⊥ : Set ↥X)

Tactic:
simp [Opens.map]

Premises used: TopologicalSpace.Opens.map
-- 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 :
  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 (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯) :
          (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