awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ GaloisConnection (β := Ideal A) Ideal.span SetLike.coe

Tactic:
have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi A _).gc
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ideal_gc : GaloisConnection (β := Ideal A) Ideal.span SetLike.coe
⊢ GaloisConnection (fun (s : Set A) ↦ zeroLocus 𝒜 s) fun (t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ) ↦
    (↑(vanishingIdeal t) : Set A)

Tactic:
simpa [zeroLocus_span, Function.comp_def] using GaloisConnection.compose ideal_gc (gc_ideal 𝒜)

Premises used: Function.comp_def, ProjectiveSpectrum.gc_ideal, ProjectiveSpectrum.zeroLocus_span, GaloisConnection.compose
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ
⊢ (fun (I : HomogeneousIdeal 𝒜) ↦ (zeroLocus 𝒜 (↑I : Set A) : Set (ProjectiveSpectrum 𝒜))) I ≤ t ↔
    I ≤ (fun (t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ) ↦ vanishingIdeal t) t

Tactic:
simpa [show I.toIdeal ≤ (vanishingIdeal t).toIdeal ↔ I ≤ vanishingIdeal t from Iff.rfl] using
    subset_zeroLocus_iff_le_vanishingIdeal t I.toIdeal

Premises used: Iff.rfl, ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, HomogeneousIdeal.toIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
s : Set A
⊢ t ⊆ zeroLocus 𝒜 s ↔ s ⊆ (↑(vanishingIdeal t) : Set A)

Tactic:
(gc_set _) s t

Premises used: ProjectiveSpectrum.gc_set
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s : Set A
⊢ s ⊆ (↑(vanishingIdeal (zeroLocus 𝒜 s)) : Set A)

Tactic:
(gc_set _).le_u_l s

Premises used: ProjectiveSpectrum.gc_set, GaloisConnection.le_u_l
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
I : Ideal A
⊢ I ≤ HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 (↑I : Set A)))

Tactic:
(gc_ideal _).le_u_l I

Premises used: GaloisConnection.le_u_l, ProjectiveSpectrum.gc_ideal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ I ≤ vanishingIdeal (zeroLocus 𝒜 (↑I : Set A))

Tactic:
(gc_homogeneousIdeal _).le_u_l I

Premises used: ProjectiveSpectrum.gc_homogeneousIdeal, GaloisConnection.le_u_l
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ t ⊆ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)

Tactic:
(gc_ideal _).l_u_le t

Premises used: ProjectiveSpectrum.gc_ideal, GaloisConnection.l_u_le
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s t : Set A
h : s ⊆ t
⊢ Subset (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 t) (zeroLocus 𝒜 s)

Tactic:
(gc_set _).monotone_l h

Premises used: ProjectiveSpectrum.gc_set, GaloisConnection.monotone_l
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s t : Ideal A
h : s ≤ t
⊢ Subset (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑t : Set A)) (zeroLocus 𝒜 (↑s : Set A))

Tactic:
(gc_ideal _).monotone_l h

Premises used: ProjectiveSpectrum.gc_ideal, GaloisConnection.monotone_l
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s t : HomogeneousIdeal 𝒜
h : s ≤ t
⊢ Subset (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑t : Set A)) (zeroLocus 𝒜 (↑s : Set A))

Tactic:
(gc_homogeneousIdeal _).monotone_l h

Premises used: ProjectiveSpectrum.gc_homogeneousIdeal, GaloisConnection.monotone_l
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s t : Set (ProjectiveSpectrum 𝒜)
h : s ⊆ t
⊢ vanishingIdeal t ≤ vanishingIdeal s

Tactic:
(gc_ideal _).monotone_u h

Premises used: GaloisConnection.monotone_u, Set.Mem, ProjectiveSpectrum.gc_ideal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑⊥ : Set A)) Set.univ

Tactic:
(gc_ideal 𝒜).l_bot

Premises used: ProjectiveSpectrum.gc_ideal, GaloisConnection.l_bot, OrderDual
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {0}) Set.univ

Tactic:
zeroLocus_bot _

Premises used: setOf, ProjectiveSpectrum.zeroLocus_bot, Set.singleton
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 ∅) Set.univ

Tactic:
(gc_set 𝒜).l_bot

Premises used: ProjectiveSpectrum.gc_set, GaloisConnection.l_bot, OrderDual
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := HomogeneousIdeal 𝒜) (vanishingIdeal ∅) ⊤

Tactic:
simpa using (gc_ideal _).u_top

Premises used: GaloisConnection.u_top, ProjectiveSpectrum.gc_ideal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s : Set A
h : 1 ∈ s
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) ∅

Tactic:
Set.eq_empty_iff_forall_notMem.mpr fun x hx =>
    (inferInstance : x.asHomogeneousIdeal.toIdeal.IsPrime).ne_top <|
      x.asHomogeneousIdeal.toIdeal.eq_top_iff_one.mpr <| hx h

Premises used: Iff.mpr, inferInstance, Ideal.eq_top_iff_one, Set.eq_empty_iff_forall_notMem, Ideal.IsPrime.ne_top, HomogeneousIdeal.toIdeal, ProjectiveSpectrum.asHomogeneousIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {1}) ∅

Tactic:
zeroLocus_empty_of_one_mem 𝒜 (Set.mem_singleton (1 : A))

Premises used: Set.mem_singleton, ProjectiveSpectrum.zeroLocus_empty_of_one_mem, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 Set.univ) ∅

Tactic:
zeroLocus_empty_of_one_mem _ (Set.mem_univ 1)

Premises used: ProjectiveSpectrum.zeroLocus_empty_of_one_mem, Set.mem_univ, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
I J : Ideal A
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(I ⊔ J) : Set A))
    (zeroLocus 𝒜 (↑I : Set A) ∩ zeroLocus 𝒜 (↑J : Set A))

Tactic:
(gc_ideal 𝒜).l_sup

Premises used: ProjectiveSpectrum.gc_ideal, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
I J : HomogeneousIdeal 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(I ⊔ J) : Set A))
    (zeroLocus 𝒜 (↑I : Set A) ∩ zeroLocus 𝒜 (↑J : Set A))

Tactic:
(gc_homogeneousIdeal 𝒜).l_sup

Premises used: ProjectiveSpectrum.gc_homogeneousIdeal, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s s' : Set A
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (s ∪ s')) (zeroLocus 𝒜 s ∩ zeroLocus 𝒜 s')

Tactic:
(gc_set 𝒜).l_sup

Premises used: ProjectiveSpectrum.gc_set, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
h : (vanishingIdeal (t ∪ t')).toIdeal = (vanishingIdeal t ⊓ vanishingIdeal t').toIdeal
⊢ vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t'

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ (vanishingIdeal (t ∪ t')).toIdeal = (vanishingIdeal t ⊓ vanishingIdeal t').toIdeal

Tactic:
(gc_ideal 𝒜).u_inf

Premises used: GaloisConnection.u_inf, ProjectiveSpectrum.gc_ideal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ (vanishingIdeal (t ∪ t')).toIdeal = (vanishingIdeal t ⊓ vanishingIdeal t').toIdeal

Tactic:
exact (gc_ideal 𝒜).u_inf

Premises used: GaloisConnection.u_inf, ProjectiveSpectrum.gc_ideal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
γ : Sort u_3
I : γ → Ideal A
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(⨆ (i : γ), I i) : Set A))
    (⋂ (i : γ), zeroLocus 𝒜 (↑(I i) : Set A))

Tactic:
(gc_ideal 𝒜).l_iSup

Premises used: iInf, Set.Mem, Set.iInter, setOf, GaloisConnection.l_iSup, ProjectiveSpectrum.gc_ideal, OrderDual
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
γ : Sort u_3
I : γ → HomogeneousIdeal 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(⨆ (i : γ), I i) : Set A))
    (⋂ (i : γ), zeroLocus 𝒜 (↑(I i) : Set A))

Tactic:
(gc_homogeneousIdeal 𝒜).l_iSup

Premises used: ProjectiveSpectrum.gc_homogeneousIdeal, iInf, Set.Mem, Set.iInter, setOf, GaloisConnection.l_iSup, OrderDual
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
γ : Sort u_3
s : γ → Set A
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (⋃ (i : γ), s i)) (⋂ (i : γ), zeroLocus 𝒜 (s i))

Tactic:
(gc_set 𝒜).l_iSup

Premises used: iInf, Set.Mem, Set.iInter, setOf, ProjectiveSpectrum.gc_set, GaloisConnection.l_iSup, OrderDual, Set.iUnion
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s : Set (Set A)
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (⋃ s' ∈ s, s')) (⋂ s' ∈ s, zeroLocus 𝒜 s')

Tactic:
simp only [zeroLocus_iUnion]

Premises used: ProjectiveSpectrum.zeroLocus_iUnion
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ Eq (α := Ideal A) (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜) (vanishingIdeal (⨅ (i : γ), t i)))
    (⨅ (i : γ), (vanishingIdeal (t i)).toIdeal)

Tactic:
(gc_ideal 𝒜).u_iInf

Premises used: GaloisConnection.u_iInf, ProjectiveSpectrum.gc_ideal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
h :
  Eq (α := Ideal A)
    (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (i : γ), vanishingIdeal (t i)))
    (⨅ (i : γ), (vanishingIdeal (t i)).toIdeal)
⊢ Eq (α := Ideal A) (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜) (vanishingIdeal (⋃ (i : γ), t i)))
    (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (i : γ), vanishingIdeal (t i)))

Tactic:
convert! (gc_ideal 𝒜).u_iInf

Premises used: GaloisConnection.u_iInf, ProjectiveSpectrum.gc_ideal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ Eq (α := Ideal A)
    (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (i : γ), vanishingIdeal (t i)))
    (⨅ (i : γ), (vanishingIdeal (t i)).toIdeal)

Tactic:
HomogeneousIdeal.toIdeal_iInf _

Premises used: HomogeneousIdeal.toIdeal_iInf
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
γ : Sort u_3
t : γ → Set (ProjectiveSpectrum 𝒜)
⊢ Eq (α := Ideal A)
    (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (i : γ), vanishingIdeal (t i)))
    (⨅ (i : γ), (vanishingIdeal (t i)).toIdeal)

Tactic:
exact HomogeneousIdeal.toIdeal_iInf _

Premises used: HomogeneousIdeal.toIdeal_iInf
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
I J : Ideal A
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(I ⊓ J) : Set A))
    (zeroLocus 𝒜 (↑I : Set A) ∪ zeroLocus 𝒜 (↑J : Set A))

Tactic:
Set.ext fun x => x.isPrime.inf_le

Premises used: Set.ext, Ideal.IsPrime.inf_le, ProjectiveSpectrum.isPrime
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s s' : Set A
rw :
  Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s')
    (zeroLocus 𝒜 (↑(Ideal.span s) : Set A) ∪ zeroLocus 𝒜 (↑(Ideal.span s') : Set A))
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s')
    (zeroLocus 𝒜 (↑(Ideal.span s ⊓ Ideal.span s') : Set A))

Tactic:
rw [zeroLocus_inf]

Premises used: ProjectiveSpectrum.zeroLocus_inf
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s s' : Set A
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s')
    (zeroLocus 𝒜 (↑(Ideal.span s) : Set A) ∪ zeroLocus 𝒜 (↑(Ideal.span s') : Set A))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
I J : Ideal A
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(I * J) : Set A))
    (zeroLocus 𝒜 (↑I : Set A) ∪ zeroLocus 𝒜 (↑J : Set A))

Tactic:
Set.ext fun x => x.isPrime.mul_le

Premises used: Set.ext, ProjectiveSpectrum.isPrime, Ideal.IsPrime.mul_le
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
I J : HomogeneousIdeal 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(I * J) : Set A))
    (zeroLocus 𝒜 (↑I : Set A) ∪ zeroLocus 𝒜 (↑J : Set A))

Tactic:
Set.ext fun x => x.isPrime.mul_le

Premises used: Set.ext, ProjectiveSpectrum.isPrime, Ideal.IsPrime.mul_le
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
x : ProjectiveSpectrum 𝒜
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {f * g}) x ↔
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {f} ∪ zeroLocus 𝒜 {g}) x

Tactic:
simpa using x.isPrime.mul_mem_iff_mem_or_mem

Premises used: ProjectiveSpectrum.isPrime, Ideal.IsPrime.mul_mem_iff_mem_or_mem
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
n : ℕ
hn : 0 < n
x : ProjectiveSpectrum 𝒜
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {f ^ n}) x ↔
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {f}) x

Tactic:
simpa using x.isPrime.pow_mem_iff_mem n hn

Premises used: Ideal.IsPrime.pow_mem_iff_mem, ProjectiveSpectrum.isPrime
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
r : A
rw :
  (∃ y ∈ (vanishingIdeal t).toIdeal, ∃ z ∈ (vanishingIdeal t').toIdeal, y + z = r) →
    ∀ x ∈ t ∩ t', r ∈ x.asHomogeneousIdeal
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')

Tactic:
rw [← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_sup, mem_vanishingIdeal,
    Submodule.mem_sup]

Premises used: ProjectiveSpectrum.mem_vanishingIdeal, HomogeneousIdeal.toIdeal_sup, Submodule.mem_sup, HomogeneousIdeal.mem_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : f ∈ (vanishingIdeal t).toIdeal
g : A
hg : g ∈ (vanishingIdeal t').toIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
rw :
  ∀ (hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal) (g : A) (hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal)
    (x : ProjectiveSpectrum 𝒜) (hxt : x ∈ t) (hxt' : x ∈ t'), f + g ∈ x.asHomogeneousIdeal
⊢ f + g ∈ x.asHomogeneousIdeal

Tactic:
rw [HomogeneousIdeal.mem_iff, mem_vanishingIdeal] at hf hg

Premises used: ProjectiveSpectrum.mem_vanishingIdeal, HomogeneousIdeal.mem_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
h₁ : f ∈ x.asHomogeneousIdeal.toSubmodule
h₂ : g ∈ x.asHomogeneousIdeal.toSubmodule
⊢ f + g ∈ x.asHomogeneousIdeal

Tactic:
apply Submodule.add_mem

Premises used: Submodule.add_mem
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asHomogeneousIdeal.toSubmodule

Tactic:
solve_by_elim
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
f : A
hf : ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
g : A
hg : ∀ x ∈ t', g ∈ x.asHomogeneousIdeal
x : ProjectiveSpectrum 𝒜
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asHomogeneousIdeal.toSubmodule

Tactic:
solve_by_elim
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
I : ProjectiveSpectrum 𝒜
rw : f ∉ (↑I.asHomogeneousIdeal : Set A) ↔ f ∉ I.asHomogeneousIdeal
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {f})ᶜ I ↔ f ∉ I.asHomogeneousIdeal

Tactic:
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, ProjectiveSpectrum.mem_zeroLocus, Set.mem_compl_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
I : ProjectiveSpectrum 𝒜
⊢ f ∉ (↑I.asHomogeneousIdeal : Set A) ↔ f ∉ I.asHomogeneousIdeal

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 Set.univ) ∅

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
rw :
  Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜))
    (⋂ (i : (↑Zs : Type u_1)), (↑i : Set (ProjectiveSpectrum 𝒜)))
⊢ Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜)) (⋂₀ Zs)

Tactic:
rw [Set.sInter_eq_iInter]

Premises used: Set.sInter_eq_iInter
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : (↑Zs : Type u_1) → Set A :=
  fun (i : (↑Zs : Type u_1)) ↦
    Classical.choose (p := fun (x : Set A) ↦ zeroLocus 𝒜 x = (↑i : Set (ProjectiveSpectrum 𝒜))) ⋯
⊢ Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜))
    (⋂ (i : (↑Zs : Type u_1)), zeroLocus 𝒜 (f i))

Tactic:
have H : (Set.iInter fun i ↦ zeroLocus 𝒜 (f i)) ∈ Set.range (zeroLocus 𝒜) :=
        ⟨_, zeroLocus_iUnion 𝒜 _⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
Zs : Set (Set (ProjectiveSpectrum 𝒜))
h : Zs ⊆ Set.range (zeroLocus 𝒜)
f : (↑Zs : Type u_1) → Set A :=
  fun (i : (↑Zs : Type u_1)) ↦
    Classical.choose (p := fun (x : Set A) ↦ zeroLocus 𝒜 x = (↑i : Set (ProjectiveSpectrum 𝒜))) ⋯
H :
  Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜))
    (⋂ (i : (↑Zs : Type u_1)), zeroLocus 𝒜 (f i))
⊢ Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜))
    (⋂ (i : (↑Zs : Type u_1)), zeroLocus 𝒜 (f i))

Tactic:
H