awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
i : ι
⊢ Continuous (Y := PrimeSpectrum ((i : ι) → R i)) fun (a : PrimeSpectrum (R i)) ↦
    sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i a)

Tactic:
exact continuous_comap (Pi.evalRingHom R i)

Premises used: PrimeSpectrum.continuous_comap, Pi.evalRingHom
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
⊢ Function.Injective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
sigmaToPi_injective R

Premises used: PrimeSpectrum.sigmaToPi_injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
⊢ Function.Injective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
exact sigmaToPi_injective R

Premises used: PrimeSpectrum.sigmaToPi_injective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
refine_3 :
  ∀ (i : ι),
    IsOpenMap (Y := PrimeSpectrum ((i : ι) → R i)) fun (a : PrimeSpectrum (R i)) ↦
      sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i a)
⊢ IsOpenMap (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
rw [isOpenMap_sigma]

Premises used: isOpenMap_sigma
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
i : ι
refine_3 :
  ∀ (s : Set (PrimeSpectrum (R i))),
    Membership.mem (γ := Set (Set (PrimeSpectrum (R i))))
        (Set.range fun (r : R i) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (R i)))) s →
      IsOpen (X := PrimeSpectrum ((i : ι) → R i)) ((fun (a : PrimeSpectrum (R i)) ↦ comap (Pi.evalRingHom R i) a) '' s)
⊢ IsOpenMap (Y := PrimeSpectrum ((i : ι) → R i)) fun (a : PrimeSpectrum (R i)) ↦
    sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i a)

Tactic:
simp only [sigmaToPi_apply, PrimeSpectrum.isTopologicalBasis_basic_opens.isOpenMap_iff]

Premises used: TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, PrimeSpectrum.isTopologicalBasis_basic_opens, PrimeSpectrum.sigmaToPi_apply
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
i : ι
f : R i
refine_3 : IsOpen (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
⊢ IsOpen (X := PrimeSpectrum ((i : ι) → R i))
    ((fun (a : PrimeSpectrum (R i)) ↦ comap (Pi.evalRingHom R i) a) ''
      (fun (r : R i) ↦ (↑(basicOpen r) : Set (PrimeSpectrum (R i)))) f)

Tactic:
rw [PrimeSpectrum.comap_evalRingHom_basicOpen]

Premises used: PrimeSpectrum.comap_evalRingHom_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
i : ι
f : R i
⊢ IsOpen (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))

Tactic:
isOpen_basicOpen

Premises used: PrimeSpectrum.isOpen_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
i : ι
f : R i
⊢ IsOpen (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))

Tactic:
exact isOpen_basicOpen

Premises used: PrimeSpectrum.isOpen_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
refine_1 : Continuous (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
refine_2 : Function.Injective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
refine_3 : IsOpenMap (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
refine_2₁ : Function.Injective (α := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
refine_3₁ refine_3₂ : IsOpenMap (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)

Tactic:
classical
  refine .of_continuous_injective_isOpenMap ?_ ?_ ?_
  · rw [continuous_sigma_iff]
    intro i
    exact continuous_comap (Pi.evalRingHom R i)
  · exact sigmaToPi_injective R
  · rw [isOpenMap_sigma]
    intro i
    simp only [sigmaToPi_apply, PrimeSpectrum.isTopologicalBasis_basic_opens.isOpenMap_iff]
    rintro - ⟨f, rfl⟩
    rw [PrimeSpectrum.comap_evalRingHom_basicOpen]
    exact isOpen_basicOpen

Premises used: TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, PrimeSpectrum.comap_evalRingHom_basicOpen, PrimeSpectrum.isOpen_basicOpen, PrimeSpectrum.isTopologicalBasis_basic_opens, continuous_sigma_iff, PrimeSpectrum.sigmaToPi_apply, isOpenMap_sigma, PrimeSpectrum.sigmaToPi_injective, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
inst_1 : Finite ι
p : (i : ι) × PrimeSpectrum (R i)
⊢ (sigmaToPiHomeo R : (a : (i : ι) × PrimeSpectrum (R i)) → PrimeSpectrum ((i : ι) → R i)) p = sigmaToPi R p

Tactic:
rfl

Premises used: PrimeSpectrum.sigmaToPi, PrimeSpectrum.comap, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
⊢ ∀ (p : PrimeSpectrum R), ∃ (f : R), (↑(basicOpen f) : Set (PrimeSpectrum R)) = {p}

Tactic:
have (p : PrimeSpectrum R) : ∃ f, (basicOpen f : Set _) = {p} :=
    have ⟨_, ⟨f, rfl⟩, hpf, hfp⟩ := isTopologicalBasis_basic_opens.isOpen_iff.mp
      (isOpen_discrete {p}) p rfl
    ⟨f, hfp.antisymm <| Set.singleton_subset_iff.mpr hpf⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
this : ∀ (p : PrimeSpectrum R), ∃ (f : R), (↑(basicOpen f) : Set (PrimeSpectrum R)) = {p}
choose :
  ∀ (f : (p : PrimeSpectrum R) → R) (hf : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}),
    ∃ (a : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x
⊢ ∃ (a : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x

Tactic:
choose f hf using this
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
a : (↑(Set.range f) : Type u)
simp_rw : IsLocalization.Away (↑a : R) (Localization.Away (↑a : R))
⊢ IsLocalization.Away (f ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) (Localization.Away (↑a : R))

Tactic:
simp_rw [e, Equiv.apply_ofInjective_symm]

Premises used: Equiv.apply_ofInjective_symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
a : (↑(Set.range f) : Type u)
⊢ IsLocalization.Away (↑a : R) (Localization.Away (↑a : R))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
⊢ ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))

Tactic:
have loc a : IsLocalization.AtPrime (Localization.Away a.1) (e.symm a).1 :=
    (isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton <| hf _).mp <| by
      simp_rw [e, Equiv.apply_ofInjective_symm]; infer_instance
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
loc :
  ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))
algE : (a : (↑(Set.range f) : Type u)) →
  Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) ≃ₐ[R]
    Localization.Away (↑a : R) :=
  fun (a : (↑(Set.range f) : Type u)) ↦
    IsLocalization.algEquiv
      (Ideal.primeCompl (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.Away (↑a : R))
⊢ Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤

Tactic:
have span_eq : Ideal.span (Set.range f) = ⊤ := iSup_basicOpen_eq_top_iff.mp <| top_unique
    fun p _ ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨p, (hf p).ge rfl⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
loc :
  ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))
algE : (a : (↑(Set.range f) : Type u)) →
  Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) ≃ₐ[R]
    Localization.Away (↑a : R) :=
  fun (a : (↑(Set.range f) : Type u)) ↦
    IsLocalization.algEquiv
      (Ideal.primeCompl (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.Away (↑a : R))
span_eq : Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
a : (↑(Set.range f) : Type u)
simp_rw :
  (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
    singleton (α := PrimeSpectrum R)
      (((Equiv.ofInjective f ⋯).symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)
simp_rw₁ :
  (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
    (↑(basicOpen (f (((Equiv.ofInjective f ⋯).symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))) :
      Set (PrimeSpectrum R))
⊢ (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
    singleton (α := PrimeSpectrum R) ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)

Tactic:
simp_rw [e, ← hf, Equiv.apply_ofInjective_symm]

Premises used: Equiv.apply_ofInjective_symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
loc :
  ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))
algE : (a : (↑(Set.range f) : Type u)) →
  Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) ≃ₐ[R]
    Localization.Away (↑a : R) :=
  fun (a : (↑(Set.range f) : Type u)) ↦
    IsLocalization.algEquiv
      (Ideal.primeCompl (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.Away (↑a : R))
span_eq : Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
⊢ ∀ (a : (↑(Set.range f) : Type u)),
    (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)

Tactic:
replace hf a : (basicOpen a.1 : Set _) = {e.symm a} := by
    simp_rw [e, ← hf, Equiv.apply_ofInjective_symm]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf_1 : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
loc :
  ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))
algE : (a : (↑(Set.range f) : Type u)) →
  Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) ≃ₐ[R]
    Localization.Away (↑a : R) :=
  fun (a : (↑(Set.range f) : Type u)) ↦
    IsLocalization.algEquiv
      (Ideal.primeCompl (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.Away (↑a : R))
span_eq : Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
hf :
  ∀ (a : (↑(Set.range f) : Type u)),
    (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)
a : (↑(Set.range f) : Type u)
⊢ Eq (α := Localization.Away ((↑a : R) * (↑a : R)))
    ((IsLocalization.Away.awayToAwayRight (↑a : R) (↑a : R) :
        (a_1 : Localization.Away (↑a : R)) → Localization.Away ((↑a : R) * (↑a : R)))
      ((fun (a : (↑(Set.range f) : Type u)) ↦
          ((algE a :
                (a_1 : Localization.AtPrime ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a).asIdeal) →
                  Localization.Away (↑a : R))
              (x ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) :
            Localization.Away (↑a : R)))
        a))
    ((IsLocalization.Away.awayToAwayLeft (↑a : R) (↑a : R) :
        (a_1 : Localization.Away (↑a : R)) → Localization.Away ((↑a : R) * (↑a : R)))
      ((fun (a : (↑(Set.range f) : Type u)) ↦
          ((algE a :
                (a_1 : Localization.AtPrime ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a).asIdeal) →
                  Localization.Away (↑a : R))
              (x ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) :
            Localization.Away (↑a : R)))
        a))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf_1 : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
loc :
  ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))
algE : (a : (↑(Set.range f) : Type u)) →
  Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) ≃ₐ[R]
    Localization.Away (↑a : R) :=
  fun (a : (↑(Set.range f) : Type u)) ↦
    IsLocalization.algEquiv
      (Ideal.primeCompl (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.Away (↑a : R))
span_eq : Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
hf :
  ∀ (a : (↑(Set.range f) : Type u)),
    (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)
a b : (↑(Set.range f) : Type u)
ne : a ≠ b
simp_rw :
  singleton (α := PrimeSpectrum R) ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R) ∩
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) b : PrimeSpectrum R) =
    (↑⊥ : Set (PrimeSpectrum R))
⊢ Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R) * (↑b : R))) ⊥

Tactic:
simp_rw [basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf, hf]

Premises used: PrimeSpectrum.basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf_1 : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
loc :
  ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))
algE : (a : (↑(Set.range f) : Type u)) →
  Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) ≃ₐ[R]
    Localization.Away (↑a : R) :=
  fun (a : (↑(Set.range f) : Type u)) ↦
    IsLocalization.algEquiv
      (Ideal.primeCompl (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.Away (↑a : R))
span_eq : Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
hf :
  ∀ (a : (↑(Set.range f) : Type u)),
    (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)
a b : (↑(Set.range f) : Type u)
ne : a ≠ b
⊢ singleton (α := PrimeSpectrum R) ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R) ∩
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) b : PrimeSpectrum R) =
    (↑⊥ : Set (PrimeSpectrum R))

Tactic:
bot_unique (fun _ ⟨ha, hb⟩ ↦ ne <| e.symm.injective (ha.symm.trans hb))

Premises used: _private.0.PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology.match_2, Membership.mem, Bot.bot, bot_unique, Equiv.injective, Equiv.symm, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf_1 : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
loc :
  ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))
algE : (a : (↑(Set.range f) : Type u)) →
  Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) ≃ₐ[R]
    Localization.Away (↑a : R) :=
  fun (a : (↑(Set.range f) : Type u)) ↦
    IsLocalization.algEquiv
      (Ideal.primeCompl (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.Away (↑a : R))
span_eq : Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
hf :
  ∀ (a : (↑(Set.range f) : Type u)),
    (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)
a b : (↑(Set.range f) : Type u)
ne : a ≠ b
⊢ singleton (α := PrimeSpectrum R) ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R) ∩
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) b : PrimeSpectrum R) =
    (↑⊥ : Set (PrimeSpectrum R))

Tactic:
exact bot_unique (fun _ ⟨ha, hb⟩ ↦ ne <| e.symm.injective (ha.symm.trans hb))

Premises used: bot_unique
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
f : (p : PrimeSpectrum R) → R
hf_1 : ∀ (p : PrimeSpectrum R), (↑(basicOpen (f p)) : Set (PrimeSpectrum R)) = {p}
e : PrimeSpectrum R ≃ (↑(Set.range f) : Type u) := Equiv.ofInjective f ⋯
loc :
  ∀ (a : (↑(Set.range f) : Type u)),
    IsLocalization.AtPrime.{u, u} (R := R) (Localization.Away (↑a : R))
      (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))
algE : (a : (↑(Set.range f) : Type u)) →
  Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) ≃ₐ[R]
    Localization.Away (↑a : R) :=
  fun (a : (↑(Set.range f) : Type u)) ↦
    IsLocalization.algEquiv
      (Ideal.primeCompl (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.AtPrime (R := R) (asIdeal ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)))
      (Localization.Away (↑a : R))
span_eq : Eq (α := Ideal R) (Ideal.span (Set.range f)) ⊤
hf :
  ∀ (a : (↑(Set.range f) : Type u)),
    (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
      singleton (α := PrimeSpectrum R)
        ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)
a b : (↑(Set.range f) : Type u)
ne : a ≠ b
⊢ IsNilpotent ((↑a : R) * (↑b : R))

Tactic:
have nil : IsNilpotent (a * b : R) := (basicOpen_eq_bot_iff _).mp <| by
        simp_rw [basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf, hf]
        exact bot_unique (fun _ ⟨ha, hb⟩ ↦ ne <| e.symm.injective (ha.symm.trans hb))