awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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)))
    (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (i : γ), vanishingIdeal (t i)))
have h : Eq (α := Ideal A) (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (i : γ), vanishingIdeal (t i)))
  (⨅ (i : γ), (vanishingIdeal (t i)).toIdeal)
Tactic: convert! (gc_ideal 𝒜).u_iInf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 ⊓ Ideal.span s') : Set A))
have rw : Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s ∪ zeroLocus 𝒜 s')
  (zeroLocus 𝒜 (↑(Ideal.span s) : Set A) ∪ zeroLocus 𝒜 (↑(Ideal.span s') : Set A))
Tactic: rw [zeroLocus_inf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
have rw : (∃ y ∈ (vanishingIdeal t).toIdeal, ∃ z ∈ (vanishingIdeal t').toIdeal, y + z = r) →
  ∀ x ∈ t ∩ t', r ∈ x.asHomogeneousIdeal
Tactic: rw [← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_sup, mem_vanishingIdeal,
    Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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'
⊢ f + g ∈ x.asHomogeneousIdeal
have 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
Tactic: rw [HomogeneousIdeal.mem_iff, mem_vanishingIdeal] at hf hg
Cleared hypotheses: hf, g, hg, x, hxt, hxt'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 + g ∈ x.asHomogeneousIdeal
have h₁ : f ∈ x.asHomogeneousIdeal.toSubmodule
Tactic: apply Submodule.add_mem
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ f + g ∈ x.asHomogeneousIdeal
have h₂ : g ∈ x.asHomogeneousIdeal.toSubmodule
Tactic: apply Submodule.add_mem
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 𝒜
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {f})ᶜ I ↔ f ∉ I.asHomogeneousIdeal
have rw : f ∉ (↑I.asHomogeneousIdeal : Set A) ↔ f ∉ I.asHomogeneousIdeal
Tactic: rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 𝒜)
⊢ Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜)) (⋂₀ Zs)
have rw : Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜))) (Set.range (zeroLocus 𝒜))
  (⋂ (i : (↑Zs : Type u_1)), (↑i : Set (ProjectiveSpectrum 𝒜)))
Tactic: rw [Set.sInter_eq_iInter]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (hypothesis)
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)), (↑i : Set (ProjectiveSpectrum 𝒜)))
have H : 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 𝒜 _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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)), (↑i : Set (ProjectiveSpectrum 𝒜)))
have 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)
Tactic: convert! H using 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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))
⊢ 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)
have h₁ : ∀ (i : (↑Zs : Type u_1)), (↑i : Set (ProjectiveSpectrum 𝒜)) = zeroLocus 𝒜 (f i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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), Uᶜ = zeroLocus 𝒜 s
have simp : IsOpen U ↔ ∃ (s : Set A), zeroLocus 𝒜 s = Uᶜ
Tactic: simp only [@eq_comm _ Uᶜ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 𝒜)
⊢ IsClosed Z ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
have rw : IsOpen Zᶜ ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
Tactic: rw [← isOpen_compl_iff, isOpen_iff, compl_compl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ IsClosed Z ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
have rw₁ : (∃ (s : Set A), Zᶜᶜ = zeroLocus 𝒜 s) ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
Tactic: rw [← isOpen_compl_iff, isOpen_iff, compl_compl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ IsClosed Z ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
have rw₂ : (∃ (s : Set A), Z = zeroLocus 𝒜 s) ↔ ∃ (s : Set A), Z = zeroLocus 𝒜 s
Tactic: rw [← isOpen_compl_iff, isOpen_iff, compl_compl]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ IsClosed (X := ProjectiveSpectrum 𝒜) (zeroLocus 𝒜 s)
have rw : ∃ (s_1 : Set A), Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) (zeroLocus 𝒜 s_1)
Tactic: rw [isClosed_iff_zeroLocus]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 𝒜)
⊢ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A) = closure t
have h₁ : zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A) ⊆ closure t
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A) = closure t
have h₂ : closure t ⊆ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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'
⊢ ∃ (s : Set A), t' = zeroLocus 𝒜 s
have rwa : ∀ (ht' : ∃ (s : Set A), t' = zeroLocus 𝒜 s) (ht : t ⊆ t'), ∃ (s : Set A), t' = zeroLocus 𝒜 s
Tactic: rwa [isClosed_iff_zeroLocus] at ht'
Cleared hypotheses: ht', ht
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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'
⊢ x ∈ t'
have h₁ : ∀ (fs : Set A) (ht' : IsClosed (X := ProjectiveSpectrum 𝒜) (zeroLocus 𝒜 fs)) (ht : t ⊆ zeroLocus 𝒜 fs),
  Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 fs) x
Tactic: obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus 𝒜 s := by rwa [isClosed_iff_zeroLocus] at ht'
Cleared hypotheses: t', ht', ht
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (hypothesis)
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
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 fs) x
have ht₁ : fs ⊆ (↑(vanishingIdeal t) : Set A)
Tactic: rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 𝒜)
⊢ closure t ⊆ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)
have h₂ : t ⊆ zeroLocus 𝒜 (↑(vanishingIdeal t) : Set A)
Tactic: rw [(isClosed_zeroLocus _ _).closure_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (hypothesis)
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 𝒜)
⊢ vanishingIdeal (closure t) = vanishingIdeal t
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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) = vanishingIdeal t
have h : (vanishingIdeal (closure t)).toIdeal = (vanishingIdeal t).toIdeal
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 𝒜)) ↔
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 {r})ᶜ x
have simp : x ∈ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜)) ↔ r ∉ (↑x.asHomogeneousIdeal : Set A)
Tactic: simp only [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 * g)) (basicOpen 𝒜 f)
have rw : LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) (basicOpen 𝒜 f)
Tactic: rw [basicOpen_mul 𝒜 f g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 * g)) (basicOpen 𝒜 g)
have rw : LE.le (α := Opens (ProjectiveSpectrum 𝒜)) (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g) (basicOpen 𝒜 g)
Tactic: rw [basicOpen_mul 𝒜 f g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 𝒜
⊢ z ∈ (↑(basicOpen 𝒜 f) : Set (ProjectiveSpectrum 𝒜)) ↔
    z ∈ (↑(⨆ (i : ℕ), basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) : Set (ProjectiveSpectrum 𝒜))
have 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
Tactic: rw [mem_coe_basicOpen, mem_coe, iSup, TopologicalSpace.Opens.mem_sSup]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 𝒜
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ ∃ (i : ℕ), ((GradedRing.proj 𝒜 i : (a : A) → A) f : A) ∉ z.asHomogeneousIdeal
have contrapose! : ∀ (H : ∀ (i : ℕ), Membership.mem (α := A) z.asHomogeneousIdeal ((GradedRing.proj 𝒜 i : (a : A) → A) f : A)),
  f ∈ z.asHomogeneousIdeal
Tactic: contrapose! hz with H
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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)
⊢ f ∈ z.asHomogeneousIdeal
have 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
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 f]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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)
⊢ f ∈ z.asHomogeneousIdeal
have 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
Tactic: classical
          rw [← DirectSum.sum_support_decompose 𝒜 f]
          apply Ideal.sum_mem _ fun i _ => H i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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
⊢ ∃ (u : Opens (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Opens (ProjectiveSpectrum 𝒜)))
        (Set.range fun (i : ℕ) ↦ basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f)) u ∧
      z ∈ u
have mp : ∀ (i : ℕ) (hi : ((GradedRing.proj 𝒜 i : (a : A) → A) f : A) ∉ 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: rcases show ∃ i, GradedRing.proj 𝒜 i f ∉ z.asHomogeneousIdeal by
          contrapose! hz with H
          classical
          rw [← DirectSum.sum_support_decompose 𝒜 f]
          apply Ideal.sum_mem _ fun i _ => H i with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
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 :
  ∃ (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
have mpr : ∀ (i : ℕ)
  (hz :
    Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜))
      ((fun (i : ℕ) ↦ (basicOpen 𝒜 ((GradedRing.proj 𝒜 i : (a : A) → A) f) : Opens (ProjectiveSpectrum 𝒜))) i) z),
  f ∉ z.asHomogeneousIdeal
Tactic: obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ IsTopologicalBasis.{u_1} (α := ProjectiveSpectrum 𝒜)
    (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜)))
have h_open : ∀ (u : Set (ProjectiveSpectrum 𝒜)),
  Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
      (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) u →
    IsOpen u
Tactic: apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
h_open :
  ∀ (u : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) u →
      IsOpen u
⊢ IsTopologicalBasis.{u_1} (α := ProjectiveSpectrum 𝒜)
    (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜)))
have h_nhds : ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
  a ∈ u →
    IsOpen u →
      ∃ (v : Set (ProjectiveSpectrum 𝒜)),
        Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
            (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
          a ∈ v ∧ v ⊆ u
Tactic: apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
hp : p ∈ U
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U
have h_nhds : ∀ (s : Set A) (hp : ∃ a ∈ s, a ∉ (↑p.asHomogeneousIdeal : Set A)) (hs : zeroLocus 𝒜 s = Uᶜ),
  ∃ (v : Set (ProjectiveSpectrum 𝒜)),
    Membership.mem (γ := Set (Set (ProjectiveSpectrum 𝒜)))
        (Set.range fun (r : A) ↦ (↑(basicOpen 𝒜 r) : Set (ProjectiveSpectrum 𝒜))) v ∧
      p ∈ v ∧ v ⊆ U
Tactic: rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp
Cleared hypotheses: hp, s, hs