awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw : LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f ⊓ basicOpen g) (basicOpen f)
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen (f * g)) (basicOpen f)

Tactic:
rw [basicOpen_mul f g]

Premises used: PrimeSpectrum.basicOpen_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f ⊓ basicOpen g) (basicOpen f)

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f ⊓ basicOpen g) (basicOpen f)

Tactic:
exact inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f g : R
rw : LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f ⊓ basicOpen g) (basicOpen g)
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen (f * g)) (basicOpen g)

Tactic:
rw [basicOpen_mul f g]

Premises used: PrimeSpectrum.basicOpen_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f ⊓ basicOpen g) (basicOpen g)

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f g : R
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f ⊓ basicOpen g) (basicOpen g)

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
n : ℕ
hn : 0 < n
⊢ (↑(basicOpen (f ^ n)) : Set (PrimeSpectrum R)) = (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
simpa using zeroLocus_singleton_pow f n hn

Premises used: PrimeSpectrum.zeroLocus_singleton_pow
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
r : R
n : ℕ
zero : LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (HPow.hPow (β := ℕ) r 0))
succ : ∀ (n : ℕ), LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (r ^ (n + 1)))
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (r ^ n))

Tactic:
cases n
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (HPow.hPow (β := ℕ) r 0))

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
r : R
n : ℕ
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen r) (basicOpen (r ^ (n + 1)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h_open :
  ∀ (u : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        u →
      IsOpen u
h_nhds :
  ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u →
      IsOpen u →
        ∃ (v : Set (PrimeSpectrum R)),
          Membership.mem (γ := Set (Set (PrimeSpectrum R)))
              (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))) v ∧
            a ∈ v ∧ v ⊆ u
⊢ TopologicalSpace.IsTopologicalBasis.{u} (α := PrimeSpectrum R)
    (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ IsOpen.{u} (X := PrimeSpectrum R) ((fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))) r)

Tactic:
isOpen_basicOpen

Premises used: PrimeSpectrum.isOpen_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ IsOpen.{u} (X := PrimeSpectrum R) ((fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))) r)

Tactic:
exact isOpen_basicOpen

Premises used: PrimeSpectrum.isOpen_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ U
s : Set R
hs : zeroLocus s = Uᶜ
h_nhds :
  ∀ (s : Set R) (hp : ∃ a ∈ s, a ∉ (↑p.asIdeal : Set R)) (hs : zeroLocus s = Uᶜ),
    ∃ (v : Set (PrimeSpectrum R)),
      Membership.mem (γ := Set (Set (PrimeSpectrum R)))
          (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))) v ∧
        p ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U

Tactic:
rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp

Premises used: compl_compl, PrimeSpectrum.mem_zeroLocus, Set.not_subset, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : ∃ a ∈ s, a ∉ (↑p.asIdeal : Set R)
hs : zeroLocus s = Uᶜ
h_nhds :
  ∀ (f : R) (hfs : f ∈ s) (hfp : f ∉ (↑p.asIdeal : Set R)),
    ∃ (v : Set (PrimeSpectrum R)),
      Membership.mem (γ := Set (Set (PrimeSpectrum R)))
          (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))) v ∧
        p ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨f, hfs, hfp⟩ := hp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ (↑p.asIdeal : Set R)
⊢ ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U

Tactic:
⟨basicOpen f, ⟨f, rfl⟩, hfp, ?_⟩

Premises used: PrimeSpectrum.basicOpen, SetLike.coe, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ (↑p.asIdeal : Set R)
h_nhds : (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ U
⊢ ∃ (v : Set (PrimeSpectrum R)),
    Membership.mem (γ := Set (Set (PrimeSpectrum R))) (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))
        v ∧
      p ∈ v ∧ v ⊆ U

Tactic:
refine ⟨basicOpen f, ⟨f, rfl⟩, hfp, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ (↑p.asIdeal : Set R)
h_nhds : Subset (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus {f})
⊢ (↑(basicOpen f) : Set (PrimeSpectrum R)) ⊆ U

Tactic:
rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]

Premises used: compl_compl, Set.compl_subset_compl, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ (↑p.asIdeal : Set R)
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus {f})

Tactic:
zeroLocus_anti_mono (Set.singleton_subset_iff.mpr hfs)

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Iff.mpr, Set.singleton_subset_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : f ∉ (↑p.asIdeal : Set R)
⊢ Subset (α := Set (PrimeSpectrum R)) (zeroLocus s) (zeroLocus {f})

Tactic:
exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr hfs)

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Iff.mpr, Set.singleton_subset_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsOpen s
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R))
    (⋃₀
      {s_1 : Set (PrimeSpectrum R) |
        Membership.mem (γ := Set (Set (PrimeSpectrum R)))
            (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))) s_1 ∧
          s_1 ⊆ s})
    (⋃ (r : R), ⋃ (_ : (↑(basicOpen r) : Set (PrimeSpectrum R)) ⊆ s), (↑(basicOpen r) : Set (PrimeSpectrum R)))

Tactic:
aesop
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ TopologicalSpace.IsTopologicalBasis.{u} (α := PrimeSpectrum R)
    (Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R)))

Tactic:
isTopologicalBasis_basic_opens (R := R)

Premises used: PrimeSpectrum.isTopologicalBasis_basic_opens
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.image (α := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe (Set.range basicOpen) =
    Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))
⊢ TopologicalSpace.IsTopologicalBasis
    (Set.image (α := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe (Set.range basicOpen))

Tactic:
convert! isTopologicalBasis_basic_opens (R := R)

Premises used: PrimeSpectrum.isTopologicalBasis_basic_opens
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
h :
  Set.range (ι := R) (Function.comp (β := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe basicOpen) =
    Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))
⊢ Set.image (α := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe (Set.range basicOpen) =
    Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
rw [← Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
⊢ Set.range (ι := R) (Function.comp (β := TopologicalSpace.Opens (PrimeSpectrum R)) SetLike.coe basicOpen) =
    Set.range fun (r : R) ↦ (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
rw : (zeroLocus {f})ᶜ = (↑⊥ : Set (PrimeSpectrum R)) ↔ IsNilpotent f
⊢ Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen f) ⊥ ↔ IsNilpotent f

Tactic:
rw [← TopologicalSpace.Opens.coe_inj, basicOpen_eq_zeroLocus_compl]

Premises used: PrimeSpectrum.basicOpen_eq_zeroLocus_compl, TopologicalSpace.Opens.coe_inj
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
simp : (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J
⊢ (zeroLocus {f})ᶜ = (↑⊥ : Set (PrimeSpectrum R)) ↔ IsNilpotent f

Tactic:
simp only [Set.eq_univ_iff_forall, Set.singleton_subset_iff, TopologicalSpace.Opens.coe_bot,
    nilpotent_iff_mem_prime, Set.compl_empty_iff, mem_zeroLocus, SetLike.mem_coe]

Premises used: Set.singleton_subset_iff, Set.eq_univ_iff_forall, PrimeSpectrum.mem_zeroLocus, Set.compl_empty_iff, SetLike.mem_coe, TopologicalSpace.Opens.coe_bot, nilpotent_iff_mem_prime
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J

Tactic:
⟨fun h I hI => h ⟨I, hI⟩, fun h ⟨I, hI⟩ => h I hI⟩

Premises used: PrimeSpectrum.mk, Membership.mem, Iff.intro, _private.0.PrimeSpectrum.basicOpen_eq_bot_iff.match_3, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J

Tactic:
exact ⟨fun h I hI => h ⟨I, hI⟩, fun h ⟨I, hI⟩ => h I hI⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
rw :
  {p : PrimeSpectrum R | Disjoint (↑(Submonoid.powers r) : Set R) (↑p.asIdeal : Set R)} =
    (↑(basicOpen r) : Set (PrimeSpectrum R))
⊢ Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S)) = (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
rw [localization_comap_range S (Submonoid.powers r)]

Premises used: Submonoid.powers, PrimeSpectrum.localization_comap_range
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
h :
  ∀ (x : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R))
        {p : PrimeSpectrum R | Disjoint (↑(Submonoid.powers r) : Set R) (↑p.asIdeal : Set R)} x ↔
      x ∈ (↑(basicOpen r) : Set (PrimeSpectrum R))
⊢ {p : PrimeSpectrum R | Disjoint (↑(Submonoid.powers r) : Set R) (↑p.asIdeal : Set R)} =
    (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
h : (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥ ↔ r ∉ x.asIdeal
⊢ Membership.mem (γ := Set (PrimeSpectrum R))
      {p : PrimeSpectrum R | Disjoint (↑(Submonoid.powers r) : Set R) (↑p.asIdeal : Set R)} x ↔
    x ∈ (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
simp only [mem_zeroLocus, basicOpen_eq_zeroLocus_compl, SetLike.mem_coe, Set.mem_setOf_eq,
    Set.singleton_subset_iff, Set.mem_compl_iff, disjoint_iff_inf_le]

Premises used: Set.singleton_subset_iff, PrimeSpectrum.mem_zeroLocus, Set.mem_setOf_eq, SetLike.mem_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, disjoint_iff_inf_le, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
h : (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥ → r ∉ x.asIdeal
h₁ : r ∉ x.asIdeal → (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥
⊢ (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥ ↔ r ∉ x.asIdeal

Tactic:
constructor
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥
h₂ : r ∈ x.asIdeal
⊢ False

Tactic:
h₁ ⟨Submonoid.mem_powers r, h₂⟩

Premises used: Set.Mem, And.intro, Submonoid.mem_powers
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : (↑(Submonoid.powers r) : Set R) ⊓ (↑x.asIdeal : Set R) ≤ ⊥
h₂ : r ∈ x.asIdeal
⊢ False

Tactic:
exact h₁ ⟨Submonoid.mem_powers r, h₂⟩

Premises used: And.intro, Submonoid.mem_powers
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : r ∉ x.asIdeal
n : ℕ
h₃ : (fun (x : ℕ) ↦ r ^ x) n ∈ (↑x.asIdeal : Set R)
⊢ Membership.mem (γ := Set R) ⊥ ((fun (x : ℕ) ↦ r ^ x) n)

Tactic:
h₁ (x.2.mem_of_pow_mem _ h₃)

Premises used: PrimeSpectrum.isPrime, Set.Mem, Ideal.IsPrime.mem_of_pow_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : r ∉ x.asIdeal
n : ℕ
h₃ : (fun (x : ℕ) ↦ r ^ x) n ∈ (↑x.asIdeal : Set R)
⊢ Membership.mem (γ := Set R) ⊥ ((fun (x : ℕ) ↦ r ^ x) n)

Tactic:
exact h₁ (x.2.mem_of_pow_mem _ h₃)

Premises used: PrimeSpectrum.isPrime, Ideal.IsPrime.mem_of_pow_mem
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
rw : IsOpen (↑(basicOpen r) : Set (PrimeSpectrum R))
⊢ IsOpen (X := PrimeSpectrum R) (Set.range (ι := PrimeSpectrum S) (comap (algebraMap R S)))

Tactic:
rw [localization_away_comap_range S r]

Premises used: PrimeSpectrum.localization_away_comap_range
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ IsOpen (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
isOpen_basicOpen

Premises used: PrimeSpectrum.isOpen_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ IsOpen (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
exact isOpen_basicOpen

Premises used: PrimeSpectrum.isOpen_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
rw :
  IsCompact (X := PrimeSpectrum R)
    (Set.range (ι := PrimeSpectrum (Localization (Submonoid.powers f)))
      (comap (algebraMap R (Localization (Submonoid.powers f)))))
⊢ IsCompact (↑(basicOpen f) : Set (PrimeSpectrum R))

Tactic:
rw [← localization_away_comap_range (Localization (Submonoid.powers f))]

Premises used: Localization, Submonoid.powers, PrimeSpectrum.localization_away_comap_range
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ IsCompact (X := PrimeSpectrum R)
    (Set.range (ι := PrimeSpectrum (Localization (Submonoid.powers f)))
      (comap (algebraMap R (Localization (Submonoid.powers f)))))

Tactic:
isCompact_range (continuous_comap _)

Premises used: PrimeSpectrum.continuous_comap, isCompact_range
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
f : R
⊢ IsCompact (X := PrimeSpectrum R)
    (Set.range (ι := PrimeSpectrum (Localization (Submonoid.powers f)))
      (comap (algebraMap R (Localization (Submonoid.powers f)))))

Tactic:
exact isCompact_range (continuous_comap _)

Premises used: PrimeSpectrum.continuous_comap, isCompact_range
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
x : R
⊢ Eq.{v + 1} (α := TopologicalSpace.Opens (PrimeSpectrum S))
    ((TopologicalSpace.Opens.comap
            { toFun := comap f, continuous_toFun := ⋯ : ContinuousMap.{v, u} (PrimeSpectrum S) (PrimeSpectrum R) } :
          (a : TopologicalSpace.Opens (PrimeSpectrum R)) → TopologicalSpace.Opens (PrimeSpectrum S))
        (basicOpen x) :
      TopologicalSpace.Opens (PrimeSpectrum S))
    (basicOpen ((f : (a : R) → S) x) : TopologicalSpace.Opens (PrimeSpectrum S))

Tactic:
rfl

Premises used: PrimeSpectrum.basicOpen, Set.Mem, setOf, Set.preimage, Not, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
f : ι → R
rw :
  ⋃ (i : ι), (↑(basicOpen (f i)) : Set (PrimeSpectrum R)) = (↑⊤ : Set (PrimeSpectrum R)) ↔
    Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
⊢ Eq.{u + 1} (α := Opens (PrimeSpectrum R)) (⨆ (i : ι), basicOpen (f i)) ⊤ ↔
    Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤

Tactic:
rw [SetLike.ext'_iff, Opens.coe_iSup]

Premises used: TopologicalSpace.Opens.coe_iSup, SetLike.ext'_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
f : ι → R
simp :
  Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), {f i}))ᶜ Set.univ ↔
    Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
⊢ ⋃ (i : ι), (↑(basicOpen (f i)) : Set (PrimeSpectrum R)) = (↑⊤ : Set (PrimeSpectrum R)) ↔
    Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤

Tactic:
simp only [PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Opens.coe_top, ← Set.compl_iInter,
    ← PrimeSpectrum.zeroLocus_iUnion]

Premises used: Set.compl_iInter, PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, TopologicalSpace.Opens.coe_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
f : ι → R
rw :
  Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), {f i})) Set.univᶜ ↔
    Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span (Set.range f)) : Set R)) ∅
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), {f i}))ᶜ Set.univ ↔
    Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤

Tactic:
rw [← PrimeSpectrum.zeroLocus_empty_iff_eq_top, compl_involutive.eq_iff]

Premises used: compl_involutive, Function.Involutive.eq_iff, PrimeSpectrum.zeroLocus_empty_iff_eq_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_1
f : ι → R
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum R)) (zeroLocus (⋃ (i : ι), {f i})) Set.univᶜ ↔
    Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.span (Set.range f)) : Set R)) ∅

Tactic:
simp only [Set.iUnion_singleton_eq_range, Set.compl_univ, PrimeSpectrum.zeroLocus_span]

Premises used: PrimeSpectrum.zeroLocus_span, Set.iUnion_singleton_eq_range, Set.compl_univ
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set R
rw : Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ (i : { x : R // x ∈ s }), basicOpen (↑i : R)) ⊤
| Eq (α := Ideal R) (Ideal.span s) ⊤

Tactic:
rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_iff]

Premises used: PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_val
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set R
conv_rhs :
  Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ i ∈ s, basicOpen i) ⊤ ↔
    Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ (i : { x : R // x ∈ s }), basicOpen (↑i : R)) ⊤
⊢ Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ i ∈ s, basicOpen i) ⊤ ↔
    Eq (α := Ideal R) (Ideal.span s) ⊤

Tactic:
conv_rhs => rw [← Subtype.range_val (s := s), ← iSup_basicOpen_eq_top_iff]

Premises used: PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_val
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
s : Set R
⊢ Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ i ∈ s, basicOpen i) ⊤ ↔
    Eq.{u + 1} (α := TopologicalSpace.Opens (PrimeSpectrum R)) (⨆ (i : { x : R // x ∈ s }), basicOpen (↑i : R)) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
⊢ f ∈ p.asIdeal.primeCompl

Tactic:
apply h ▸ Set.mem_singleton p
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
refine :
  ∀ (r : R) (hr : r ∈ p.asIdeal.primeCompl), ∃ (m : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) m ∧ r ∣ m
⊢ IsLocalization.AtPrime (Localization.Away f) p.asIdeal

Tactic:
refine .of_le_of_exists_dvd (.powers f) _
      (Submonoid.powers_le.mpr <| by apply h ▸ Set.mem_singleton p) fun r hr ↦ ?_
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
f : R
p : PrimeSpectrum R
h : Eq (α := Set (PrimeSpectrum R)) (TopologicalSpace.Opens.carrier (basicOpen f)) {p}
r : R
hr : r ∈ p.asIdeal.primeCompl
contrapose! :
  ∀ (hr : ∀ (m : R) (_ : Membership.mem (γ := Submonoid R) (Submonoid.powers f) m), ¬r ∣ m), r ∉ p.asIdeal.primeCompl
⊢ ∃ (m : R), Membership.mem (γ := Submonoid R) (Submonoid.powers f) m ∧ r ∣ m

Tactic:
contrapose! hr