awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
⊢ I = ⊤ → I.support = ⊥

Tactic:
simp +contextual
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
refine : ∀ (H : I.support = ⊥) (U : (↑X.affineOpens : Type u)), ideal ⊤ U ≤ I.ideal U
⊢ I.support = ⊥ ↔ I = ⊤

Tactic:
refine ⟨fun H ↦ top_le_iff.mp fun U ↦ ?_, by simp +contextual⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
H : I.support = ⊥
U : (↑X.affineOpens : Type u)
⊢ Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊆
    (↑⊥ : Set ↥X)

Tactic:
have := (U.2.fromSpec_image_zeroLocus _).trans_subset
    ((zeroLocus_inter_subset_supportSet I U).trans H.le)
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
H : I.support = ⊥
U : (↑X.affineOpens : Type u)
this :
  Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊆
    (↑⊥ : Set ↥X)
⊢ Eq (α := Set ↥(Spec Γ(X, (↑U : X.Opens))))
    (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ∅

Tactic:
simp only [Set.subset_empty_iff, Set.image_eq_empty, Closeds.coe_bot] at this

Premises used: TopologicalSpace.Closeds.coe_bot, Set.image_eq_empty, Set.subset_empty_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
H : I.support = ⊥
U : (↑X.affineOpens : Type u)
this :
  Eq (α := Set ↥(Spec Γ(X, (↑U : X.Opens))))
    (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ∅
⊢ ideal ⊤ U ≤ I.ideal U

Tactic:
simp [PrimeSpectrum.zeroLocus_empty_iff_eq_top.mp this]

Premises used: Iff.mp, PrimeSpectrum.zeroLocus_empty_iff_eq_top
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I_2 J_1 K I J : X.IdealSheafData
⊢ ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ((I.ideal * J.ideal) U) =
      (I.ideal * J.ideal) (X.affineBasicOpen f)

Tactic:
simp [Ideal.map_mul, map_ideal_basicOpen]

Premises used: Ideal.map_mul, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I_2 J_1 K I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
⊢ x ∈ I.supportSet ∪ J.supportSet ↔ x ∈ X.zeroLocus (↑((I.ideal * J.ideal) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
simp [-mem_zeroLocus_iff, zeroLocus_mul, mem_support_iff_of_mem hxU]

Premises used: AlgebraicGeometry.Scheme.zeroLocus_mul, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, AlgebraicGeometry.Scheme.mem_zeroLocus_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I_2 J K I : X.IdealSheafData
n : ℕ
⊢ ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ((I.ideal ^ n) U) =
      (I.ideal ^ n) (X.affineBasicOpen f)

Tactic:
simp [Ideal.map_pow, map_ideal_basicOpen]

Premises used: Ideal.map_pow, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I_2 J K I : X.IdealSheafData
n : ℕ
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
zero :
  x ∈ X.zeroLocus (↑(HPow.hPow (β := ℕ) I.ideal 0 U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
    x ∈ if Eq (α := ℕ) 0 0 then ∅ else I.supportSet
succ :
  ∀ (n : ℕ),
    (x ∈ X.zeroLocus (↑((I.ideal ^ n) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
        x ∈ if n = 0 then ∅ else I.supportSet) →
      (x ∈ X.zeroLocus (↑((I.ideal ^ (n + 1)) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
        x ∈ if n + 1 = 0 then ∅ else I.supportSet)
⊢ x ∈ X.zeroLocus (↑((I.ideal ^ n) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔ x ∈ if n = 0 then ∅ else I.supportSet

Tactic:
induction n
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I_2 J K I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
⊢ x ∈ X.zeroLocus (↑(HPow.hPow (β := ℕ) I.ideal 0 U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
    x ∈ if Eq (α := ℕ) 0 0 then ∅ else I.supportSet

Tactic:
simp_all [-mem_zeroLocus_iff, zeroLocus_mul,
      pow_succ, mem_support_iff_of_mem hxU]

Premises used: AlgebraicGeometry.Scheme.zeroLocus_mul, pow_succ, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, AlgebraicGeometry.Scheme.mem_zeroLocus_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I_2 J K I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
n : ℕ
h : x ∈ X.zeroLocus (↑((I.ideal ^ n) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔ x ∈ if n = 0 then ∅ else I.supportSet
⊢ x ∈ X.zeroLocus (↑((I.ideal ^ (n + 1)) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
    x ∈ if n + 1 = 0 then ∅ else I.supportSet

Tactic:
simp_all [-mem_zeroLocus_iff, zeroLocus_mul,
      pow_succ, mem_support_iff_of_mem hxU]

Premises used: AlgebraicGeometry.Scheme.zeroLocus_mul, pow_succ, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, AlgebraicGeometry.Scheme.mem_zeroLocus_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ (I * J).ideal = I.ideal * J.ideal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ (I * J).support = I.support ⊔ J.support

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
n : ℕ
⊢ (I ^ n).ideal = I.ideal ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
n : ℕ
⊢ (I ^ (n + 1)).support = I.support

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, iInf, iSup, Set.iInter, setOf, npowRec, AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff, rfl, ite
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) I 0).support = I.support
succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), (I ^ (n + 1)).support = I.support
⊢ (I ^ n).support = I.support

Tactic:
cases n
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
hn : Ne (α := ℕ) 0 0
⊢ (HPow.hPow (β := ℕ) I 0).support = I.support

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
n : ℕ
hn : n + 1 ≠ 0
⊢ (I ^ (n + 1)).support = I.support

Tactic:
simp_all
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)), x_1 ∈ (⊤ * I).ideal x ↔ x_1 ∈ I.ideal x
⊢ ⊤ * I = I

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
x : (↑X.affineOpens : Type u)
x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)
⊢ x_1 ∈ (⊤ * I).ideal x ↔ x_1 ∈ I.ideal x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)), x_1 ∈ (I * ⊤).ideal x ↔ x_1 ∈ I.ideal x
⊢ I * ⊤ = I

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
x : (↑X.affineOpens : Type u)
x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)
⊢ x_1 ∈ (I * ⊤).ideal x ↔ x_1 ∈ I.ideal x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)), x_1 ∈ (⊥ * I).ideal x ↔ x_1 ∈ ideal ⊥ x
⊢ ⊥ * I = ⊥

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
x : (↑X.affineOpens : Type u)
x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)
⊢ x_1 ∈ (⊥ * I).ideal x ↔ x_1 ∈ ideal ⊥ x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)), x_1 ∈ (I * ⊥).ideal x ↔ x_1 ∈ ideal ⊥ x
⊢ I * ⊥ = ⊥

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
x : (↑X.affineOpens : Type u)
x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)
⊢ x_1 ∈ (I * ⊥).ideal x ↔ x_1 ∈ ideal ⊥ x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J K : X.IdealSheafData
h : ∀ (U : (↑X.affineOpens : Type u)), (I * (J ⊔ K)).ideal U = (I * J ⊔ I * K).ideal U
⊢ I * (J ⊔ K) = I * J ⊔ I * K

Tactic:
ext U : 2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J K : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (I * (J ⊔ K)).ideal U = (I * J ⊔ I * K).ideal U

Tactic:
mul_add _ _ _

Premises used: Set.Mem, setOf, mul_add
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J K : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (I * (J ⊔ K)).ideal U = (I * J ⊔ I * K).ideal U

Tactic:
exact mul_add _ _ _

Premises used: mul_add
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J K : X.IdealSheafData
h : ∀ (U : (↑X.affineOpens : Type u)), ((I ⊔ J) * K).ideal U = (I * K ⊔ J * K).ideal U
⊢ (I ⊔ J) * K = I * K ⊔ J * K

Tactic:
ext U : 2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J K : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ ((I ⊔ J) * K).ideal U = (I * K ⊔ J * K).ideal U

Tactic:
add_mul _ _ _

Premises used: add_mul, Set.Mem, setOf
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J K : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ ((I ⊔ J) * K).ideal U = (I * K ⊔ J * K).ideal U

Tactic:
exact add_mul _ _ _

Premises used: add_mul
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I J K x : X.IdealSheafData
h :
  ∀ (x_1 : (↑X.affineOpens : Type u)) (x_2 : (↑Γ(X, (↑x_1 : X.Opens)) : Type u)),
    x_2 ∈ (HPow.hPow (β := ℕ) x 0).ideal x_1 ↔ x_2 ∈ ideal 1 x_1
⊢ HPow.hPow (β := ℕ) x 0 = 1

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I J K x : X.IdealSheafData
x_1 : (↑X.affineOpens : Type u)
x_2 : (↑Γ(X, (↑x_1 : X.Opens)) : Type u)
⊢ x_2 ∈ (HPow.hPow (β := ℕ) x 0).ideal x_1 ↔ x_2 ∈ ideal 1 x_1

Tactic:
simp [show (1 : X.IdealSheafData) = ⊤ from rfl]

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I J K : X.IdealSheafData
x : ℕ
x_1 : X.IdealSheafData
h :
  ∀ (x_2 : (↑X.affineOpens : Type u)) (x_3 : (↑Γ(X, (↑x_2 : X.Opens)) : Type u)),
    x_3 ∈ (x_1 ^ (x + 1)).ideal x_2 ↔ x_3 ∈ (x_1 ^ x * x_1).ideal x_2
⊢ x_1 ^ (x + 1) = x_1 ^ x * x_1

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I J K : X.IdealSheafData
x : ℕ
x_1 : X.IdealSheafData
x_2 : (↑X.affineOpens : Type u)
x_3 : (↑Γ(X, (↑x_2 : X.Opens)) : Type u)
⊢ x_3 ∈ (x_1 ^ (x + 1)).ideal x_2 ↔ x_3 ∈ (x_1 ^ x * x_1).ideal x_2

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := X.IdealSheafData) 0 ⊥

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ I + J = I ⊔ J

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : X.IdealSheafData
I : Ideal (↑Γ(X, ⊤) : Type u)
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
rw :
  Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (F := (↑Γ(X, ⊤) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ (homOfLE ⋯).op))) I)
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (Ideal.map (F :=
            (↑(X.presheaf.obj (Opposite.op ⊤)) : Type u) →+* (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) I :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (Ideal.map (F :=
              (↑(X.presheaf.obj (Opposite.op ⊤)) : Type u) →+*
                (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u))
              (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) I :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (Ideal.map (F :=
            (↑(X.presheaf.obj (Opposite.op ⊤)) : Type u) →+* (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) I :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))

Tactic:
rw [Ideal.map_map, ← CommRingCat.hom_comp, ← Functor.map_comp]

Premises used: CommRingCat.hom_comp, Ideal.map_map, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : X.IdealSheafData
I : Ideal (↑Γ(X, ⊤) : Type u)
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (F := (↑Γ(X, ⊤) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ (homOfLE ⋯).op))) I)
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (Ideal.map (F :=
            (↑(X.presheaf.obj (Opposite.op ⊤)) : Type u) →+* (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) I :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : X.IdealSheafData
I : Ideal (↑Γ(X, ⊤) : Type u)
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
⊢ x ∈ X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u)) ↔
    x ∈
      X.zeroLocus
        (↑((fun (U : (↑X.affineOpens : Type u)) ↦
                (Ideal.map (F :=
                    (↑(X.presheaf.obj (Opposite.op ⊤)) : Type u) →+*
                      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u))
                    (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) I :
                  Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
              U) :
          Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
simp only [Ideal.map, zeroLocus_span, zeroLocus_map, Set.mem_union, Set.mem_compl_iff,
        SetLike.mem_coe, hxU, not_true_eq_false, iff_self_or, IsEmpty.forall_iff]

Premises used: Set.mem_union, not_true_eq_false, Ideal.map, AlgebraicGeometry.Scheme.zeroLocus_map, iff_self_or, SetLike.mem_coe, AlgebraicGeometry.Scheme.zeroLocus_span, Set.mem_compl_iff, IsEmpty.forall_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsAffine X
I J : X.IdealSheafData
H :
  LE.le (α := Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u))
    (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
    (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
U : (↑X.affineOpens : Type u)
rw :
  LE.le (α := (fun (U : (↑X.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)) U)
    (Ideal.map (R := (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u)) (F :=
      (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u) →+*
        (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯)))
    (Ideal.map (R := (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u)) (F :=
      (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u) →+*
        (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯)))
⊢ I.ideal U ≤ J.ideal U

Tactic:
rw [← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) I (le_top (a := U.1)),
    ← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) J (le_top (a := U.1))]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, le_top
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsAffine X
I J : X.IdealSheafData
H :
  LE.le (α := Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u))
    (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
    (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
U : (↑X.affineOpens : Type u)
⊢ LE.le (α := (fun (U : (↑X.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)) U)
    (Ideal.map (R := (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u)) (F :=
      (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u) →+*
        (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯)))
    (Ideal.map (R := (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u)) (F :=
      (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u) →+*
        (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯)))

Tactic:
Ideal.map_mono H

Premises used: Set.Mem, Ideal.map_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsAffine X
I J : X.IdealSheafData
H :
  LE.le (α := Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u))
    (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
    (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
U : (↑X.affineOpens : Type u)
⊢ LE.le (α := (fun (U : (↑X.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)) U)
    (Ideal.map (R := (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u)) (F :=
      (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u) →+*
        (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯)))
    (Ideal.map (R := (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u)) (F :=
      (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u) →+*
        (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
      (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯)))

Tactic:
exact Ideal.map_mono H

Premises used: Ideal.map_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsAffine X
I J : X.IdealSheafData
H :
  Eq (α := Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u))
    (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
    (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
⊢ I = J

Tactic:
(le_of_isAffine H.le).antisymm (le_of_isAffine H.ge)

Premises used: Eq.ge, AlgebraicGeometry.Scheme.IdealSheafData.le_of_isAffine, LE.le.antisymm, Eq.le
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : X.IdealSheafData
inst : IsAffine X
I : X.IdealSheafData
⊢ ideal
      (ofIdealTop
        ((fun (x : X.IdealSheafData) ↦
            (x.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) :
              Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u)))
          I))
      (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) =
    I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : X.IdealSheafData
inst : IsAffine X
I : Ideal (↑Γ(X, ⊤) : Type u)
⊢ (fun (x : X.IdealSheafData) ↦
        (x.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) :
          Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u)))
      (ofIdealTop I) =
    I

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
inst : IsAffine X
⊢ ∀ (x y : X.IdealSheafData),
    (x * y).ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) =
      HMul.hMul (α := Ideal (↑Γ(X, ⊤) : Type u)) (β := Ideal (↑Γ(X, ⊤) : Type u))
        (x.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) :
          Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u))
        (y.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
inst : IsAffine X
⊢ ∀ (x y : X.IdealSheafData),
    (x + y).ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) =
      HAdd.hAdd (α := Ideal (↑Γ(X, ⊤) : Type u)) (β := Ideal (↑Γ(X, ⊤) : Type u))
        (x.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) :
          Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u))
        (y.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsAffine X
I : X.IdealSheafData
⊢ Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    ((equivOfIsAffine : (a : X.IdealSheafData) → Ideal (↑Γ(X, ⊤) : Type u)) I : Ideal (↑Γ(X, ⊤) : Type u))
    (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) :
      Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsAffine X
I : Ideal (↑Γ(X, ⊤) : Type u)
⊢ (OrderRingIso.symm equivOfIsAffine : (a : Ideal (↑Γ(X, ⊤) : Type u)) → X.IdealSheafData) I = ofIdealTop I

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
hx : x ∈ (↑U : X.Opens)
⊢ x ∈ I.supportSet ↔
    x ∈
      X.zeroLocus
        (↑((fun (U : (↑X.affineOpens : Type u)) ↦ (I.ideal U).radical) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
simp only [mem_supportSet_iff_of_mem hx, AlgebraicGeometry.Scheme.zeroLocus_radical]

Premises used: AlgebraicGeometry.Scheme.zeroLocus_radical, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
⊢ I.radical.support = I.support

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, setOf, AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff, AlgebraicGeometry.Scheme.IdealSheafData.radical, Ideal.radical, rfl