awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
x : ↥X
hxV : x ∈ (↑(↑V : X.Opens) : Set ↥X)
hxU : x ∈ (↑(↑U : X.Opens) : Set ↥X)
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
this :
  Membership.mem (α := (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (γ :=
    Submodule (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
        s :
      (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (x ∈
      X.basicOpen
        (HMul.hMul (α := (↑Γ(X, X.basicOpen f) : Type u)) (β := (↑Γ(X, X.basicOpen f) : Type u))
          ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
              s :
            (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
          ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
              (↑(s',
                      Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                        Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                        ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
                (↑Γ(X, (↑U : X.Opens)) : Type u)) :
            (↑Γ(X, X.basicOpen f) : Type u)))) =
    (x ∈
      X.basicOpen (U := X.basicOpen f)
        ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
          (↑(s',
                  Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯).1 :
            (↑Γ(X, (↑U : X.Opens)) : Type u))))
refine : x ∈ X.basicOpen (↑s' : (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ False

Tactic:
refine hx s' s'.2 ?_

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
x : ↥X
hxV : x ∈ (↑(↑V : X.Opens) : Set ↥X)
hxU : x ∈ (↑(↑U : X.Opens) : Set ↥X)
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
this :
  Membership.mem (α := (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (γ :=
    Submodule (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
        s :
      (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s' : ↥(I.ideal U)
hs' :
  (x ∈
      X.basicOpen
        (HMul.hMul (α := (↑Γ(X, X.basicOpen f) : Type u)) (β := (↑Γ(X, X.basicOpen f) : Type u))
          ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
              s :
            (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
          ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
              (↑(s',
                      Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                        Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                        ((fun (x : ℕ) ↦ f ^ x) 0) ⋯).2 :
                (↑Γ(X, (↑U : X.Opens)) : Type u)) :
            (↑Γ(X, X.basicOpen f) : Type u)))) =
    (x ∈
      X.basicOpen (U := X.basicOpen f)
        ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
          (↑(s',
                  Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) 0) ⋯).1 :
            (↑Γ(X, (↑U : X.Opens)) : Type u))))
⊢ x ∈ X.basicOpen (↑s' : (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
simpa [RingHom.algebraMap_toAlgebra, ← hfg, hxf, hxs, Scheme.basicOpen_pow] using hs'

Premises used: AlgebraicGeometry.Scheme.basicOpen_pow, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
x : ↥X
hxV : x ∈ (↑(↑V : X.Opens) : Set ↥X)
hxU : x ∈ (↑(↑U : X.Opens) : Set ↥X)
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
this :
  Membership.mem (α := (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (γ :=
    Submodule (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
        s :
      (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (x ∈
      X.basicOpen
        (HMul.hMul (α := (↑Γ(X, X.basicOpen f) : Type u)) (β := (↑Γ(X, X.basicOpen f) : Type u))
          ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
              s :
            (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
          ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
              (↑(s',
                      Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                        Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                        ((fun (x : ℕ) ↦ f ^ x) (n + 1)) ⋯).2 :
                (↑Γ(X, (↑U : X.Opens)) : Type u)) :
            (↑Γ(X, X.basicOpen f) : Type u)))) =
    (x ∈
      X.basicOpen (U := X.basicOpen f)
        ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
          (↑(s',
                  Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) (n + 1)) ⋯).1 :
            (↑Γ(X, (↑U : X.Opens)) : Type u))))
⊢ x ∈ X.basicOpen (↑s' : (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
simpa [RingHom.algebraMap_toAlgebra, ← hfg, hxf, hxs, Scheme.basicOpen_pow] using hs'

Premises used: AlgebraicGeometry.Scheme.basicOpen_pow, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥X
U : (↑X.affineOpens : Type u)
hxU : x ∈ (↑U : X.Opens)
⊢ x ∈ I.supportSet ↔ x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
⟨I.supportSet_eq_iInter_zeroLocus ▸ fun h ↦ Set.iInter_subset _ U h,
    fun h ↦ I.zeroLocus_inter_subset_supportSet U ⟨h, hxU⟩⟩

Premises used: Eq.rec, AlgebraicGeometry.Scheme.zeroLocus, SetLike.coe, And.intro, Iff.intro, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, Set.iInter_subset, Eq.symm, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
h :
  ∀ (x : ↥X),
    x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
      x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
⊢ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
pos :
  ∀ (hxU : x ∈ (↑U : X.Opens)),
    x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
      x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
neg :
  ∀ (hxU : x ∉ (↑U : X.Opens)),
    x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
      x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
⊢ x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
by_cases hxU : x ∈ U.1

Premises used: Subtype.val
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
⊢ x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
simp [hxU, mem_supportSet_iff_of_mem hxU]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∉ (↑U : X.Opens)
⊢ x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
simp [hxU]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
rw :
  ∀ (i : (↑X.affineOpens : Type u)),
    IsClosed (X := ↥(↑i : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑i : X.Opens)) ⁻¹' I.supportSet)
⊢ IsClosed I.supportSet

Tactic:
rw [TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage (iSup_affineOpens_eq_top X)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ IsClosed (X := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)

Tactic:
⟨(X.zeroLocus (U := U.1) (I.ideal U))ᶜ, (X.zeroLocus_isClosed _).isOpen_compl, ?_⟩

Premises used: IsClosed.isOpen_compl, Compl.compl, AlgebraicGeometry.Scheme.zeroLocus, SetLike.coe, And.intro, Exists.intro, IsClosed.mk, AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
refine :
  Eq (α := Set ↥(↑U : X.Opens))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
      (X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))ᶜ)
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)ᶜ
⊢ IsClosed (X := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)

Tactic:
refine ⟨(X.zeroLocus (U := U.1) (I.ideal U))ᶜ, (X.zeroLocus_isClosed _).isOpen_compl, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
simp :
  Eq (α := Set ↥(↑U : X.Opens))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)
⊢ Eq (α := Set ↥(↑U : X.Opens))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
      (X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))ᶜ)
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)ᶜ

Tactic:
simp only [Set.preimage_compl, compl_inj_iff]

Premises used: Set.preimage_compl, compl_inj_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Set.image (α := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)))
      (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
        X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
    Set.image (α := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)))
      (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)
⊢ Eq (α := Set ↥(↑U : X.Opens))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)

Tactic:
apply Subtype.val_injective.image_injective

Premises used: Subtype.val_injective, Function.Injective.image_injective
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Set.image (α := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)))
      (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
        X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
    Set.image (α := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)))
      (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)

Tactic:
simp [Set.image_preimage_eq_inter_range, I.supportSet_inter]

Premises used: Set.image_preimage_eq_inter_range, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
⊢ (↑I.support : Set ↥X) =
    ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
I.supportSet_eq_iInter_zeroLocus

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥X
⊢ x ∈ I.supportSet ↔ x ∈ I.support

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥X
⊢ x ∈ I.support ↔
    ∀ (U : (↑X.affineOpens : Type u)), x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
(Set.ext_iff.mp I.supportSet_eq_iInter_zeroLocus _).trans Set.mem_iInter

Premises used: Set.Mem, Set.mem_iInter, Iff.mp, Iff.trans, Set.ext_iff, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥X
U : (↑X.affineOpens : Type u)
h : x ∈ (↑U : X.Opens)
⊢ x ∈ I.support ↔ x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
simpa [-mem_zeroLocus_iff, h] using congr(x ∈ $(I.supportSet_inter U))

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, AlgebraicGeometry.Scheme.mem_zeroLocus_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
I.supportSet_inter U

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
ideal : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
supportSet : Set ↥X
supportSet_inter :
  ∀ (U : (↑X.affineOpens : Type u)),
    ∀ x ∈ (↑U : X.Opens), x ∈ supportSet ↔ x ∈ X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
change : supportSet = I'.supportSet
⊢ supportSet = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
change supportSet = I'.supportSet

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.supportSet
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
ideal : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
supportSet : Set ↥X
supportSet_inter :
  ∀ (U : (↑X.affineOpens : Type u)),
    ∀ x ∈ (↑U : X.Opens), x ∈ supportSet ↔ x ∈ X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
h : ∀ (x : ↥X), x ∈ supportSet ↔ x ∈ I'.supportSet
⊢ supportSet = I'.supportSet

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
ideal : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
supportSet : Set ↥X
supportSet_inter :
  ∀ (U : (↑X.affineOpens : Type u)),
    ∀ x ∈ (↑U : X.Opens), x ∈ supportSet ↔ x ∈ X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
x : ↥X
h :
  ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)),
    x ∈ supportSet ↔ x ∈ I'.supportSet
⊢ x ∈ supportSet ↔ x ∈ I'.supportSet

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
ideal : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
supportSet : Set ↥X
supportSet_inter :
  ∀ (U : (↑X.affineOpens : Type u)),
    ∀ x ∈ (↑U : X.Opens), x ∈ supportSet ↔ x ∈ X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
⊢ x ∈ supportSet ↔ x ∈ I'.supportSet

Tactic:
(supportSet_inter ⟨U, hU⟩ x hxU).trans
      (I'.mem_support_iff_of_mem (U := ⟨U, hU⟩) hxU).symm

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, Subtype.mk, Iff.trans, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
ideal : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
supportSet : Set ↥X
supportSet_inter :
  ∀ (U : (↑X.affineOpens : Type u)),
    ∀ x ∈ (↑U : X.Opens), x ∈ supportSet ↔ x ∈ X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
⊢ x ∈ supportSet ↔ x ∈ I'.supportSet

Tactic:
exact (supportSet_inter ⟨U, hU⟩ x hxU).trans
      (I'.mem_support_iff_of_mem (U := ⟨U, hU⟩) hxU).symm

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, Subtype.mk, Iff.trans, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := Closeds ↥X) (support ⊤) ⊥

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := Closeds ↥X) (support ⊥) ⊤

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, Set.univ, setOf, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
rw :
  Subset.{u} (α := Set ↥X)
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(J.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ J.support ≤ I.support

Tactic:
rw [← SetLike.coe_subset_coe, I.coe_support_eq_eq_iInter_zeroLocus,
    J.coe_support_eq_eq_iInter_zeroLocus]

Premises used: SetLike.coe_subset_coe, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
⊢ Subset.{u} (α := Set ↥X)
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(J.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
Set.iInter_mono fun U ↦ X.zeroLocus_mono (h U)

Premises used: AlgebraicGeometry.Scheme.zeroLocus_mono, Set.iInter_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
⊢ Subset.{u} (α := Set ↥X)
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(J.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
exact Set.iInter_mono fun U ↦ X.zeroLocus_mono (h U)

Premises used: AlgebraicGeometry.Scheme.zeroLocus_mono, Set.iInter_mono