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 𝒜
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))
h₁ :
  Eq.{u_1 + 1} (α := (↑Zs : Type u_1) → Set (ProjectiveSpectrum 𝒜))
    (fun (i : (↑Zs : Type u_1)) ↦ (↑i : Set (ProjectiveSpectrum 𝒜))) fun (i : (↑Zs : Type u_1)) ↦ zeroLocus 𝒜 (f i)
⊢ Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜))
    (⋂ (i : (↑Zs : Type u_1)), (↑i : Set (ProjectiveSpectrum 𝒜)))

Tactic:
convert! H using 2
-- 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))
h₁ : ∀ (i : (↑Zs : Type u_1)), (↑i : Set (ProjectiveSpectrum 𝒜)) = zeroLocus 𝒜 (f i)
⊢ Eq.{u_1 + 1} (α := (↑Zs : Type u_1) → Set (ProjectiveSpectrum 𝒜))
    (fun (i : (↑Zs : Type u_1)) ↦ (↑i : Set (ProjectiveSpectrum 𝒜))) fun (i : (↑Zs : Type u_1)) ↦ zeroLocus 𝒜 (f i)

Tactic:
funext i
-- 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))
i : (↑Zs : Type u_1)
⊢ (↑i : Set (ProjectiveSpectrum 𝒜)) = zeroLocus 𝒜 (f i)

Tactic:
(Classical.choose_spec (h i.2)).symm

Premises used: Classical.choose_spec, Eq.symm, Subtype.property
-- 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))
i : (↑Zs : Type u_1)
⊢ (↑i : Set (ProjectiveSpectrum 𝒜)) = zeroLocus 𝒜 (f i)

Tactic:
exact (Classical.choose_spec (h i.2)).symm

Premises used: Classical.choose_spec, Eq.symm, Subtype.property
-- 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
⊢ Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜)) (zeroLocus 𝒜 s ∪ zeroLocus 𝒜 t)

Tactic:
⟨_, (union_zeroLocus 𝒜 s t).symm⟩

Premises used: Set.Mem, setOf, ProjectiveSpectrum.union_zeroLocus, Exists.intro, Set.range, Eq.symm
-- 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
⊢ Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜)) (zeroLocus 𝒜 s ∪ zeroLocus 𝒜 t)

Tactic:
exact ⟨_, (union_zeroLocus 𝒜 s t).symm⟩
-- 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 𝒜
U : Set (ProjectiveSpectrum 𝒜)
simp : IsOpen U ↔ ∃ (s : Set A), zeroLocus 𝒜 s = Uᶜ
⊢ IsOpen U ↔ ∃ (s : Set A), Uᶜ = zeroLocus 𝒜 s

Tactic:
simp only [@eq_comm _ Uᶜ]

Premises used: eq_comm
-- 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 𝒜
U : Set (ProjectiveSpectrum 𝒜)
⊢ IsOpen U ↔ ∃ (s : Set A), zeroLocus 𝒜 s = Uᶜ

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 𝒜
Z : Set (ProjectiveSpectrum 𝒜)
rw : IsOpen Zᶜ ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
rw₁ : (∃ (s : Set A), Zᶜᶜ = zeroLocus 𝒜 s) ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
rw₂ rw₃ : (∃ (s : Set A), Z = zeroLocus 𝒜 s) ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
⊢ IsClosed Z ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff, compl_compl]

Premises used: compl_compl, ProjectiveSpectrum.isOpen_iff, isOpen_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 𝒜
s : Set A
rw : ∃ (s_1 : Set A), Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) (zeroLocus 𝒜 s_1)
⊢ IsClosed (X := ProjectiveSpectrum 𝒜) (zeroLocus 𝒜 s)

Tactic:
rw [isClosed_iff_zeroLocus]

Premises used: ProjectiveSpectrum.isClosed_iff_zeroLocus
-- 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_1 : Set A), Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) (zeroLocus 𝒜 s_1)

Tactic:
⟨s, rfl⟩

Premises used: Exists.intro, 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 𝒜
s : Set A
⊢ ∃ (s_1 : Set A), Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) (zeroLocus 𝒜 s_1)

Tactic:
exact ⟨s, 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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
h₁ : zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A) ⊆ closure t
h₂ : closure t ⊆ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)
⊢ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A) = closure t

Tactic:
apply Set.Subset.antisymm

Premises used: Set.Subset.antisymm
-- 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 𝒜)
x : ProjectiveSpectrum 𝒜
hx : Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)) x
t' : Set (ProjectiveSpectrum 𝒜)
ht' : IsClosed t'
ht : t ⊆ t'
rwa rwa₁ rwa₂ rwa₃ : ∀ (ht' : ∃ (s : Set A), t' = zeroLocus 𝒜 s) (ht : t ⊆ t'), ∃ (s : Set A), t' = zeroLocus 𝒜 s
⊢ ∃ (s : Set A), t' = zeroLocus 𝒜 s

Tactic:
rwa [isClosed_iff_zeroLocus] at ht'

Premises used: ProjectiveSpectrum.isClosed_iff_zeroLocus
-- 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 𝒜)
x : ProjectiveSpectrum 𝒜
hx : Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)) x
t' : Set (ProjectiveSpectrum 𝒜)
ht' : IsClosed t'
ht : t ⊆ t'
h₁ :
  ∀ (fs : Set A) (ht' : IsClosed (X := ProjectiveSpectrum 𝒜) (zeroLocus 𝒜 fs)) (ht : t ⊆ zeroLocus 𝒜 fs),
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 fs) x
⊢ x ∈ t'

Tactic:
obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus 𝒜 s := by rwa [isClosed_iff_zeroLocus] at ht'

Premises used: 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 𝒜
t : Set (ProjectiveSpectrum 𝒜)
x : ProjectiveSpectrum 𝒜
hx : Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)) x
fs : Set A
ht' : IsClosed (X := ProjectiveSpectrum 𝒜) (zeroLocus 𝒜 fs)
ht : t ⊆ zeroLocus 𝒜 fs
⊢ fs ⊆ (↑(vanishingIdeal t) : Set A)

Tactic:
rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht

Premises used: ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal
-- 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 𝒜)
x : ProjectiveSpectrum 𝒜
hx : Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)) x
fs : Set A
ht' : IsClosed (X := ProjectiveSpectrum 𝒜) (zeroLocus 𝒜 fs)
ht : fs ⊆ (↑(vanishingIdeal t) : Set A)
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 fs) x

Tactic:
Set.Subset.trans ht hx

Premises used: Set.Mem, Set.Subset.trans, setOf, ProjectiveSpectrum.zeroLocus
-- 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 𝒜)
x : ProjectiveSpectrum 𝒜
hx : Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)) x
fs : Set A
ht' : IsClosed (X := ProjectiveSpectrum 𝒜) (zeroLocus 𝒜 fs)
ht : fs ⊆ (↑(vanishingIdeal t) : Set A)
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 fs) x

Tactic:
exact Set.Subset.trans ht hx

Premises used: Set.Subset.trans
-- 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 𝒜)
h₂ : t ⊆ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)
⊢ closure t ⊆ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)

Tactic:
rw [(isClosed_zeroLocus _ _).closure_subset_iff]

Premises used: ProjectiveSpectrum.isClosed_zeroLocus, IsClosed.closure_subset_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 : Set (ProjectiveSpectrum 𝒜)
⊢ t ⊆ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)

Tactic:
subset_zeroLocus_vanishingIdeal 𝒜 t

Premises used: ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal
-- 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:
exact subset_zeroLocus_vanishingIdeal 𝒜 t

Premises used: ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal
-- 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 𝒜)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A))) = (vanishingIdeal t).toIdeal

Tactic:
have : (vanishingIdeal (zeroLocus 𝒜 (vanishingIdeal t))).toIdeal = _ := (gc_ideal 𝒜).u_l_u_eq_u t
-- 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 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A))) = (vanishingIdeal t).toIdeal
h : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ vanishingIdeal (closure 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 : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A))) = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal

Tactic:
rw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this

Premises used: ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- 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 𝒜)
this : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal

Tactic:
this
-- 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 𝒜)
this : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
⊢ (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal

Tactic:
exact this
-- 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
x : ProjectiveSpectrum 𝒜
⊢ Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f) x ↔ f ∉ x.asHomogeneousIdeal

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- 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
x : ProjectiveSpectrum 𝒜
⊢ x ∈ (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜)) ↔ f ∉ x.asHomogeneousIdeal

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- 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 𝒜
a : A
⊢ IsOpen (↑(basicOpen 𝒜 a) : Set (ProjectiveSpectrum 𝒜))

Tactic:
(basicOpen 𝒜 a).isOpen

Premises used: ProjectiveSpectrum.basicOpen, TopologicalSpace.Opens.isOpen
-- 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 𝒜
r : A
x : ProjectiveSpectrum 𝒜
simp : x ∈ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜)) ↔ r ∉ (↑x.asHomogeneousIdeal : Set A)
⊢ x ∈ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜)) ↔
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {r})ᶜ x

Tactic:
simp only [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 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜)) ↔ r ∉ (↑x.asHomogeneousIdeal : Set A)

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 𝒜
⊢ (↑(basicOpen 𝒜 1) : Set (ProjectiveSpectrum 𝒜)) = (↑⊤ : Set (ProjectiveSpectrum 𝒜))

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 𝒜
⊢ (↑(basicOpen 𝒜 0) : Set (ProjectiveSpectrum 𝒜)) = (↑⊥ : Set (ProjectiveSpectrum 𝒜))

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 𝒜
f g : A
⊢ (↑(basicOpen 𝒜 (f * g)) : Set (ProjectiveSpectrum 𝒜)) =
    (↑(basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) : Set (ProjectiveSpectrum 𝒜))

Tactic:
simp [zeroLocus_singleton_mul]

Premises used: ProjectiveSpectrum.zeroLocus_singleton_mul
-- 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
rw : LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) (basicOpen 𝒜 f)
⊢ LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 (f * g)) (basicOpen 𝒜 f)

Tactic:
rw [basicOpen_mul 𝒜 f g]

Premises used: ProjectiveSpectrum.basicOpen_mul
-- 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
⊢ LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) (basicOpen 𝒜 f)

Tactic:
inf_le_left

Premises used: inf_le_left
-- 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
⊢ LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) (basicOpen 𝒜 f)

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- 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
rw : LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) (basicOpen 𝒜 g)
⊢ LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 (f * g)) (basicOpen 𝒜 g)

Tactic:
rw [basicOpen_mul 𝒜 f g]

Premises used: ProjectiveSpectrum.basicOpen_mul
-- 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
⊢ LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) (basicOpen 𝒜 g)

Tactic:
inf_le_right

Premises used: inf_le_right
-- 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
⊢ LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) (basicOpen 𝒜 g)

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- 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
⊢ (↑(basicOpen 𝒜 (f ^ n)) : Set (ProjectiveSpectrum 𝒜)) = (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜))

Tactic:
simpa using zeroLocus_singleton_pow 𝒜 f n hn

Premises used: ProjectiveSpectrum.zeroLocus_singleton_pow
-- 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
z : ProjectiveSpectrum 𝒜
rw :
  f ∉ z.asHomogeneousIdeal ↔
    ∃ (u : Opens (ProjectiveSpectrum 𝒜)),
      Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
          (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
        z ∈ u
⊢ z ∈ (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜)) ↔
    z ∈ (↑(⨆ (i : ℕ), basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) : Set (ProjectiveSpectrum 𝒜))

Tactic:
rw [mem_coe_basicOpen, mem_coe, iSup, TopologicalSpace.Opens.mem_sSup]

Premises used: iSup, TopologicalSpace.Opens.mem_sSup, SetLike.mem_coe, ProjectiveSpectrum.mem_coe_basicOpen
-- 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
z : ProjectiveSpectrum 𝒜
mp :
  f ∉ z.asHomogeneousIdeal →
    ∃ (u : Opens (ProjectiveSpectrum 𝒜)),
      Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
          (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
        z ∈ u
mpr :
  (∃ (u : Opens (ProjectiveSpectrum 𝒜)),
      Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
          (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
        z ∈ u) →
    f ∉ z.asHomogeneousIdeal
⊢ f ∉ z.asHomogeneousIdeal ↔
    ∃ (u : Opens (ProjectiveSpectrum 𝒜)),
      Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
          (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
        z ∈ u

Tactic:
constructor
-- 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
z : ProjectiveSpectrum 𝒜
hz : f ∉ z.asHomogeneousIdeal
contrapose! :
  ∀ (H : ∀ (i : ℕ), Membership.mem (α := A) z.asHomogeneousIdeal ((GradedRing.proj 𝒜 i : (a : A) → A) f : A)),
    f ∈ z.asHomogeneousIdeal
⊢ ∃ (i : ℕ), ((GradedRing.proj 𝒜 i : (a : A) → A) f : A) ∉ z.asHomogeneousIdeal

Tactic:
contrapose! hz with H
-- 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
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), Membership.mem (α := A) z.asHomogeneousIdeal ((GradedRing.proj 𝒜 i : (a : A) → A) f : A)
rw :
  ∑ i ∈ DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) f),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) f : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∈
    z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal

Tactic:
rw [← DirectSum.sum_support_decompose 𝒜 f]

Premises used: DirectSum.sum_support_decompose
-- 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
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), Membership.mem (α := A) z.asHomogeneousIdeal ((GradedRing.proj 𝒜 i : (a : A) → A) f : A)
⊢ ∑ i ∈ DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) f),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) f : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∈
    z.asHomogeneousIdeal

Tactic:
apply Ideal.sum_mem _ fun i _ => H i

Premises used: Ideal.sum_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
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), Membership.mem (α := A) z.asHomogeneousIdeal ((GradedRing.proj 𝒜 i : (a : A) → A) f : A)
rw rw₁ rw₂ :
  ∑ i ∈ DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) f),
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) f : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∈
    z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal

Tactic:
classical
          rw [← DirectSum.sum_support_decompose 𝒜 f]
          apply Ideal.sum_mem _ fun i _ => H i

Premises used: Ideal.sum_mem