awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
r : (↑Γ(Y, U) : Type u)
⊢ f ⁻¹ᵁ Y.basicOpen r =
    X.basicOpen (U := f ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r)

Tactic:
LocallyRingedSpace.preimage_basicOpen f.toLRSHom r

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
⊢ f ⁻¹ᵁ Y.basicOpen r =
    X.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r)

Tactic:
preimage_basicOpen ..

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : (↑Γ(Y, V) : Type u)
simp :
  X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE e).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ V) : Type u)) → (↑Γ(X, U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app f V) :
              (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
            s :
          (↑Γ(X, f ⁻¹ᵁ V) : Type u))) =
    U ⊓
      X.basicOpen (U := f ⁻¹ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app f V) :
            (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
          s)
⊢ X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appLE f V U e) :
          (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, U) : Type u))
        s) =
    U ⊓ f ⁻¹ᵁ Y.basicOpen s

Tactic:
simp only [preimage_basicOpen, Hom.appLE, CommRingCat.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, CommRingCat.comp_apply, AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : (↑Γ(Y, V) : Type u)
rw rw₁ :
  U ⊓
      X.basicOpen (U := f ⁻¹ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app f V) :
            (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
          s) =
    U ⊓
      X.basicOpen (U := f ⁻¹ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app f V) :
            (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
          s)
⊢ X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE e).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ V) : Type u)) → (↑Γ(X, U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app f V) :
              (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
            s :
          (↑Γ(X, f ⁻¹ᵁ V) : Type u))) =
    U ⊓
      X.basicOpen (U := f ⁻¹ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app f V) :
            (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
          s)

Tactic:
rw [basicOpen_res]

Premises used: AlgebraicGeometry.Scheme.basicOpen_res
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
⊢ X.basicOpen (U := U) 0 = ⊥

Tactic:
LocallyRingedSpace.basicOpen_zero _ U

Premises used: AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u_1)
⊢ X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

Tactic:
RingedSpace.basicOpen_mul _ _ _

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_mul, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f : (↑Γ(X, U) : Type u_1)
n : ℕ
h : 0 < n
⊢ X.basicOpen (f ^ n) = X.basicOpen f

Tactic:
RingedSpace.basicOpen_pow _ _ _ h

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_pow, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u_1)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
⊢ x ∈ U

Tactic:
have hxU : x ∈ U := X.basicOpen_le _ hx
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u_1)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
simp :
  ∀
    (hx :
      IsUnit
        (HAdd.hAdd (α := (↑(X.presheaf.stalk x) : 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) (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))
              f :
            (↑(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))
              g :
            (↑(X.presheaf.stalk x) : Type u_1)))),
    IsUnit (M := (↑(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))
            f :
          (↑(X.presheaf.stalk x) : Type u_1)) ∨
      IsUnit (M := (↑(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))
            g :
          (↑(X.presheaf.stalk x) : Type u_1))
⊢ x ∈ X.basicOpen f ∨ x ∈ X.basicOpen g

Tactic:
simp only [Scheme.mem_basicOpen _ _ _ hxU, map_add] at hx ⊢

Premises used: map_add, AlgebraicGeometry.Scheme.mem_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u_1)
x : ↥X
hxU : x ∈ U
hx :
  IsUnit
    (HAdd.hAdd (α := (↑(X.presheaf.stalk x) : 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) (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))
          f :
        (↑(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))
          g :
        (↑(X.presheaf.stalk x) : Type u_1)))
⊢ IsUnit (M := (↑(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))
          f :
        (↑(X.presheaf.stalk x) : Type u_1)) ∨
    IsUnit (M := (↑(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))
          g :
        (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
IsLocalRing.isUnit_or_isUnit_of_isUnit_add hx

Premises used: IsLocalRing.isUnit_or_isUnit_of_isUnit_add
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u_1)
x : ↥X
hxU : x ∈ U
hx :
  IsUnit
    (HAdd.hAdd (α := (↑(X.presheaf.stalk x) : 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) (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))
          f :
        (↑(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))
          g :
        (↑(X.presheaf.stalk x) : Type u_1)))
⊢ IsUnit (M := (↑(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))
          f :
        (↑(X.presheaf.stalk x) : Type u_1)) ∨
    IsUnit (M := (↑(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))
          g :
        (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
exact IsLocalRing.isUnit_or_isUnit_of_isUnit_add hx

Premises used: IsLocalRing.isUnit_or_isUnit_of_isUnit_add
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f : (↑Γ(X, U) : Type u_1)
hf : IsUnit f
⊢ X.basicOpen f = U

Tactic:
RingedSpace.basicOpen_of_isUnit _ hf

Premises used: AlgebraicGeometry.RingedSpace.basicOpen_of_isUnit, AlgebraicGeometry.Scheme.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
⊢ X.basicOpen (U := U) 1 = U

Tactic:
X.basicOpen_of_isUnit isUnit_one

Premises used: AlgebraicGeometry.Scheme.basicOpen_of_isUnit, isUnit_one
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
⊢ Spec.map f ⁻¹ᵁ PrimeSpectrum.basicOpen r =
    PrimeSpectrum.basicOpen
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) f :
          (a : (↑R : Type u_1)) → (↑S : Type u_1))
        r)

Tactic:
rfl

Premises used: PrimeSpectrum.basicOpen, Set.Mem, setOf, Set.preimage, Not, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
⊢ X.zeroLocus s = ⋂ f ∈ s, (X.basicOpen f).carrierᶜ

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.RingedSpace.zeroLocus, AlgebraicGeometry.Scheme.zeroLocus, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
⊢ IsClosed (X.zeroLocus s)

Tactic:
X.toRingedSpace.zeroLocus_isClosed s

Premises used: AlgebraicGeometry.RingedSpace.zeroLocus_isClosed, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, AlgebraicGeometry.Scheme.zeroLocus, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
f : (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (U := U) {f} = (↑(X.basicOpen f) : Set ↥X)ᶜ

Tactic:
X.toRingedSpace.zeroLocus_singleton f

Premises used: Set.Mem, setOf, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, AlgebraicGeometry.Scheme.zeroLocus, AlgebraicGeometry.RingedSpace.zeroLocus_singleton, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
⊢ X.zeroLocus (U := U) ∅ = Set.univ

Tactic:
X.toRingedSpace.zeroLocus_empty_eq_univ

Premises used: AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, AlgebraicGeometry.Scheme.zeroLocus, AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
⊢ x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
X.toRingedSpace.mem_zeroLocus_iff s x

Premises used: Set.Mem, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, AlgebraicGeometry.RingedSpace.mem_zeroLocus_iff, AlgebraicGeometry.Scheme.zeroLocus, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
⊢ ∀ (x : ↥X), ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U

Tactic:
have (x : X) : ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U := fun _ _ h ↦ X.basicOpen_le _ h
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
this : ∀ (x : ↥X), ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U
⊢ Codisjoint (X.zeroLocus s) (↑U : Set ↥X)

Tactic:
simpa [codisjoint_iff_le_sup, Set.ext_iff, or_iff_not_imp_left]

Premises used: codisjoint_iff_le_sup, Classical.or_iff_not_imp_left, Set.ext_iff
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
h : ∀ (x : ↥X), x ∈ X.zeroLocus (↑(Ideal.span s) : Set (↑Γ(X, U) : Type u)) ↔ x ∈ X.zeroLocus s
⊢ X.zeroLocus (↑(Ideal.span s) : Set (↑Γ(X, U) : Type u)) = X.zeroLocus s

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
h :
  (∀ (f : (↑Γ(X, U) : Type u)), Membership.mem (γ := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) f → x ∉ X.basicOpen f) ↔
    ∀ f ∈ s, x ∉ X.basicOpen f
⊢ x ∈ X.zeroLocus (↑(Ideal.span s) : Set (↑Γ(X, U) : Type u)) ↔ x ∈ X.zeroLocus s

Tactic:
simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]

Premises used: SetLike.mem_coe, AlgebraicGeometry.Scheme.mem_zeroLocus_iff
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
⊢ (∀ (f : (↑Γ(X, U) : Type u)), Membership.mem (γ := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) f → x ∉ X.basicOpen f) ↔
    ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
⟨fun H f hfs ↦ H f (Ideal.subset_span hfs), fun H f ↦ Submodule.span_induction H ?_ ?_ ?_⟩

Premises used: Ideal.subset_span, Submodule.span_induction, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
h : ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f : (↑Γ(X, U) : Type u)), x ∉ X.basicOpen (U := U) 0
h₁ :
  ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f x_1 y : (↑Γ(X, U) : Type u))
    (hx :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s)
        x_1)
    (hy :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s) y),
    x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)
h₂ :
  ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f a x_1 : (↑Γ(X, U) : Type u))
    (hx :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s)
        x_1),
    x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)
⊢ (∀ (f : (↑Γ(X, U) : Type u)), Membership.mem (γ := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) f → x ∉ X.basicOpen f) ↔
    ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
refine ⟨fun H f hfs ↦ H f (Ideal.subset_span hfs), fun H f ↦ Submodule.span_induction H ?_ ?_ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
h : x ∉ ⊥
⊢ x ∉ X.basicOpen (U := U) 0

Tactic:
simp only [Scheme.basicOpen_zero]

Premises used: AlgebraicGeometry.Scheme.basicOpen_zero
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
⊢ x ∉ ⊥

Tactic:
not_false

Premises used: Set.Mem, not_false
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
⊢ x ∉ ⊥

Tactic:
exact not_false

Premises used: not_false
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
⊢ ∀ (x_1 y : (↑Γ(X, U) : Type u))
    (hx :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s)
        x_1)
    (hy :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s) y),
    x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)

Tactic:
fun a b _ _ ha hb H ↦ (X.basicOpen_add_le a b H).elim ha hb

Premises used: AlgebraicGeometry.Scheme.basicOpen_add_le, Or.elim, Not
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
⊢ ∀ (x_1 y : (↑Γ(X, U) : Type u))
    (hx :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s)
        x_1)
    (hy :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s) y),
    x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)

Tactic:
exact fun a b _ _ ha hb H ↦ (X.basicOpen_add_le a b H).elim ha hb

Premises used: AlgebraicGeometry.Scheme.basicOpen_add_le, Or.elim
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
⊢ ∀ (a x_1 : (↑Γ(X, U) : Type u))
    (hx :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s)
        x_1),
    x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)

Tactic:
simp +contextual
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s t : Set (↑Γ(X, U) : Type u)
simp :
  Eq.{u + 1} (α := Set ↥X) (⋂ a ∈ s, ⋂ b ∈ t, (X.basicOpen (a * b)).carrierᶜ)
    ((⋂ f ∈ s, (X.basicOpen f).carrierᶜ) ∪ ⋂ f ∈ t, (X.basicOpen f).carrierᶜ)
⊢ X.zeroLocus (s * t) = X.zeroLocus s ∪ X.zeroLocus t

Tactic:
simp only [← Set.image2_mul, zeroLocus_def, Set.biInter_image2]

Premises used: Set.biInter_image2, AlgebraicGeometry.Scheme.zeroLocus_def, Set.image2_mul
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s t : Set (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := Set ↥X) (⋂ a ∈ s, ⋂ b ∈ t, (X.basicOpen (a * b)).carrierᶜ)
    ((⋂ f ∈ s, (X.basicOpen f).carrierᶜ) ∪ ⋂ f ∈ t, (X.basicOpen f).carrierᶜ)

Tactic:
simp [Set.compl_inter, ← Set.union_iInter₂, ← Set.iInter₂_union]

Premises used: Set.compl_inter, Set.iInter₂_union, Set.union_iInter₂
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
rw :
  X.zeroLocus (↑(I * J) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus
      (↑(HMul.hMul (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span (↑I : Set (↑Γ(X, U) : Type u)))
            (Ideal.span (↑J : Set (↑Γ(X, U) : Type u)))) :
        Set (↑Γ(X, U) : Type u))
⊢ X.zeroLocus (↑(I * J) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))

Tactic:
rw [← X.zeroLocus_setMul, ← X.zeroLocus_span (U := U) (↑I * ↑J), ← Ideal.span_mul_span]

Premises used: HMul.hMul, AlgebraicGeometry.Scheme.zeroLocus_setMul, Ideal.span_mul_span, AlgebraicGeometry.Scheme.zeroLocus_span
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (↑(I * J) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus
      (↑(HMul.hMul (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span (↑I : Set (↑Γ(X, U) : Type u)))
            (Ideal.span (↑J : Set (↑Γ(X, U) : Type u)))) :
        Set (↑Γ(X, U) : Type u))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set (↑Γ(X, V) : Type u)
h :
  ∀ (x : ↥X),
    x ∈
        X.zeroLocus (U := U)
          ((⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
            s) ↔
      x ∈ X.zeroLocus s ∪ (↑U : Set ↥X)ᶜ
⊢ X.zeroLocus (U := U)
      ((⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
        s) =
    X.zeroLocus s ∪ (↑U : Set ↥X)ᶜ

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set (↑Γ(X, V) : Type u)
x : ↥X
this : (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f
⊢ x ∈
      X.zeroLocus (U := U)
        ((⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
          s) ↔
    x ∈ X.zeroLocus s ∪ (↑U : Set ↥X)ᶜ

Tactic:
simpa [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set (↑Γ(X, V) : Type u)
x : ↥X
h : (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f
⊢ x ∈
      X.zeroLocus (U := U)
        ((⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
          s) ↔
    x ∈ X.zeroLocus s ∪ (↑U : Set ↥X)ᶜ

Tactic:
suffices (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → (∀ f ∈ s, x ∉ X.basicOpen f) by
    simpa [or_iff_not_imp_right]
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set (↑Γ(X, V) : Type u)
x : ↥X
⊢ (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
grind
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
i : U = V
s : Set (↑Γ(X, V) : Type u)
h :
  ∀ (x : ↥X),
    x ∈
        X.zeroLocus (U := U)
          ((⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom i)))) :
              (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
            s) ↔
      x ∈ X.zeroLocus s
⊢ X.zeroLocus (U := U)
      ((⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom i)))) :
          (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
        s) =
    X.zeroLocus s

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
i : U = V
s : Set (↑Γ(X, V) : Type u)
x : ↥X
⊢ x ∈
      X.zeroLocus (U := U)
        ((⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom i)))) :
            (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
          s) ↔
    x ∈ X.zeroLocus s

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s t : Set (↑Γ(X, U) : Type u)
h : s ⊆ t
simp : ∀ (x : ↥X), (∀ f ∈ t, x ∉ X.basicOpen f) → ∀ f ∈ s, x ∉ X.basicOpen f
⊢ X.zeroLocus t ⊆ X.zeroLocus s

Tactic:
simp only [Set.subset_def, Scheme.mem_zeroLocus_iff]

Premises used: Set.subset_def, AlgebraicGeometry.Scheme.mem_zeroLocus_iff