awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
nil : IsNilpotent ((↑a : R) * (↑b : R))
⊢ Eq (α := Localization.Away ((↑a : R) * (↑b : R)))
    ((IsLocalization.Away.awayToAwayRight (↑a : R) (↑b : R) :
        (a_1 : Localization.Away (↑a : R)) → Localization.Away ((↑a : R) * (↑b : 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 (↑b : R) (↑a : R) :
        (a_1 : Localization.Away (↑b : R)) → Localization.Away ((↑a : R) * (↑b : 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)))
        b))

Tactic:
apply (IsLocalization.subsingleton (M := .powers (a * b : R)) nil).elim

Premises used: Subsingleton.elim
-- 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)
obtain :
  ∀ (r : R)
    (eq :
      ∀ (a : (↑(Set.range f) : Type u)),
        Eq (α := Localization.Away (↑a : R))
          ((algebraMap R (Localization.Away (↑a : R)) : (a_1 : R) → Localization.Away (↑a : R)) r :
            Localization.Away (↑a : R))
          ((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 : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x
⊢ ∃ (a : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x

Tactic:
obtain ⟨r, eq, -⟩ := Localization.existsUnique_algebraMap_eq_of_span_eq_top _ span_eq
    (fun a ↦ algE a (x _)) fun a b ↦ by
      obtain rfl | ne := eq_or_ne a b; · rfl
      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))
      apply (IsLocalization.subsingleton (M := .powers (a * b : R)) nil).elim

Premises used: Localization.existsUnique_algebraMap_eq_of_span_eq_top, Equiv.symm, DFunLike.coe
-- 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)
r : R
eq :
  ∀ (a : (↑(Set.range f) : Type u)),
    Eq (α := Localization.Away (↑a : R))
      ((algebraMap R (Localization.Away (↑a : R)) : (a_1 : R) → Localization.Away (↑a : R)) r :
        Localization.Away (↑a : R))
      ((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 : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x

Tactic:
⟨r, funext fun I ↦ ?_⟩

Premises used: funext, Exists.intro
-- 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)
r : R
eq :
  ∀ (a : (↑(Set.range f) : Type u)),
    Eq (α := Localization.Away (↑a : R))
      ((algebraMap R (Localization.Away (↑a : R)) : (a_1 : R) → Localization.Away (↑a : R)) r :
        Localization.Away (↑a : R))
      ((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))
refine : ∀ (I : PrimeSpectrum R), (toPiLocalization R : (a : R) → PiLocalization R) r I = x I
⊢ ∃ (a : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x

Tactic:
refine ⟨r, funext fun I ↦ ?_⟩
-- 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)
r : R
eq :
  ∀ (a : (↑(Set.range f) : Type u)),
    Eq (α := Localization.Away (↑a : R))
      ((algebraMap R (Localization.Away (↑a : R)) : (a_1 : R) → Localization.Away (↑a : R)) r :
        Localization.Away (↑a : R))
      ((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))
I : PrimeSpectrum R
⊢ Eq (α := Localization.Away (M := R) (↑((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I) : R))
    ((algebraMap R (Localization.Away (M := R) (↑((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I) : R)) :
          (a : R) → Localization.Away (↑((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I) : R))
        r :
      Localization.Away (M := R) (↑((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I) : R))
    ((algE ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I) :
          (a :
              Localization.AtPrime
                ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
                    ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)).asIdeal) →
            Localization.Away (↑((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I) : R))
        (x
          ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
            ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I))) :
      Localization.Away (M := R) (↑((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I) : R))

Tactic:
have := eq (e I)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
rw :
  Function.Surjective (α := R) (β := MaximalSpectrum.PiLocalization R)
    (⇑(AlgHom.comp (piLocalizationToMaximal R) (toPiLocalization R)) : (a : R) → MaximalSpectrum.PiLocalization R)
⊢ Function.Surjective (α := R) (β := MaximalSpectrum.PiLocalization R)
    (⇑(MaximalSpectrum.toPiLocalization R) : (a : R) → MaximalSpectrum.PiLocalization R)

Tactic:
rw [← piLocalizationToMaximal_comp_toPiLocalization]

Premises used: PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
⊢ Function.Surjective (α := R) (β := MaximalSpectrum.PiLocalization R)
    (⇑(AlgHom.comp (piLocalizationToMaximal R) (toPiLocalization R)) : (a : R) → MaximalSpectrum.PiLocalization R)

Tactic:
(piLocalizationToMaximal_surjective R).comp
    (toPiLocalization_surjective_of_discreteTopology R)

Premises used: PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, PrimeSpectrum.piLocalizationToMaximal_surjective, Quotient.mk', Function.Surjective.comp, OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
⊢ Function.Surjective (α := R) (β := MaximalSpectrum.PiLocalization R)
    (⇑(AlgHom.comp (piLocalizationToMaximal R) (toPiLocalization R)) : (a : R) → MaximalSpectrum.PiLocalization R)

Tactic:
exact (piLocalizationToMaximal_surjective R).comp
    (toPiLocalization_surjective_of_discreteTopology R)

Premises used: PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, PrimeSpectrum.piLocalizationToMaximal_surjective, Function.Surjective.comp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : R
⊢ Eq (α := MaximalSpectrum.PiLocalization R)
    ((MaximalSpectrum.toPiLocalizationEquiv R : (a : R) → MaximalSpectrum.PiLocalization R) x :
      MaximalSpectrum.PiLocalization R)
    ((algebraMap R (MaximalSpectrum.PiLocalization R) : (a : R) → MaximalSpectrum.PiLocalization R) x :
      MaximalSpectrum.PiLocalization R)

Tactic:
rfl

Premises used: Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : R
I : MaximalSpectrum R
⊢ Eq (α := Localization.AtPrime I.asIdeal)
    ((MaximalSpectrum.toPiLocalizationEquiv R : (a : R) → MaximalSpectrum.PiLocalization R) x I :
      Localization.AtPrime I.asIdeal)
    ((algebraMap R (Localization.AtPrime I.asIdeal) : (a : R) → Localization.AtPrime I.asIdeal) x :
      Localization.AtPrime I.asIdeal)

Tactic:
rfl

Premises used: Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
inst : CommSemiring R
⊢ DiscreteTopology.{u_1} (PrimeSpectrum R) ↔
    Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)

Tactic:
⟨fun _ ↦ toPiLocalization_surjective_of_discreteTopology _,
    discreteTopology_of_toLocalization_surjective⟩

Premises used: PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, PrimeSpectrum.discreteTopology_of_toLocalization_surjective, Iff.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
inst : CommSemiring R
⊢ DiscreteTopology.{u_1} (PrimeSpectrum R) ↔
    Function.Bijective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)

Tactic:
discreteTopology_iff_toPiLocalization_surjective.trans
    (and_iff_right <| toPiLocalization_injective _).symm

Premises used: and_iff_right, PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective, Iff.trans, PrimeSpectrum.toPiLocalization_injective, Iff.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
⊢ Function.Bijective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)

Tactic:
discreteTopology_iff_toPiLocalization_bijective.mp inferInstance

Premises used: inferInstance, Iff.mp, PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : R
⊢ Eq (α := PiLocalization R) ((toPiLocalizationEquiv R : (a : R) → PiLocalization R) x : PiLocalization R)
    ((algebraMap R (PiLocalization R) : (a : R) → PiLocalization R) x : PiLocalization R)

Tactic:
rfl

Premises used: Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : R
I : PrimeSpectrum R
⊢ Eq (α := Localization (M := R) I.asIdeal.primeCompl)
    ((toPiLocalizationEquiv R : (a : R) → PiLocalization R) x I : Localization (M := R) I.asIdeal.primeCompl)
    ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) x :
      Localization (M := R) I.asIdeal.primeCompl)

Tactic:
rfl

Premises used: Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x y : PrimeSpectrum R
rw : x.asIdeal ≤ y.asIdeal ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (closure {x}) y
rw₁ : x.asIdeal ≤ y.asIdeal ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(vanishingIdeal {x}) : Set R)) y
rw₂ : x.asIdeal ≤ y.asIdeal ↔ (↑(vanishingIdeal {x}) : Set R) ⊆ (↑y.asIdeal : Set R)
rw₃ : x.asIdeal ≤ y.asIdeal ↔ (↑x.asIdeal : Set R) ⊆ (↑y.asIdeal : Set R)
rw₄ rw₅ : x.asIdeal ≤ y.asIdeal ↔ x.asIdeal ≤ y.asIdeal
⊢ x ≤ y ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (closure {x}) y

Tactic:
rw [← asIdeal_le_asIdeal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus,
    vanishingIdeal_singleton, SetLike.coe_subset_coe]

Premises used: PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe, PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, PrimeSpectrum.asIdeal_le_asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
inst : CommSemiring R
x y : PrimeSpectrum R
⊢ x ≤ y ↔ x ⤳ y

Tactic:
(le_iff_mem_closure x y).trans specializes_iff_mem_closure.symm

Premises used: specializes_iff_mem_closure, PrimeSpectrum.le_iff_mem_closure, Iff.trans, Iff.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ T0Space.{u} (PrimeSpectrum R)

Tactic:
⟨nhdsOrderEmbedding.inj'⟩

Premises used: PrimeSpectrum.nhdsOrderEmbedding, Function.Embedding.inj', RelEmbedding.toEmbedding, T0Space.mk
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
⊢ PrespectralSpace.{u} (PrimeSpectrum R)

Tactic:
.of_isTopologicalBasis' isTopologicalBasis_basic_opens isCompact_basicOpen

Premises used: PrespectralSpace.of_isTopologicalBasis', PrimeSpectrum.isTopologicalBasis_basic_opens, PrimeSpectrum.isCompact_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x y : PrimeSpectrum R
h : x ⤳ y
a : R
ha : a ∈ y.asIdeal.primeCompl
rw :
  ∀ (h : (↑y.asIdeal : Set R)ᶜ ⊆ (↑x.asIdeal : Set R)ᶜ) (a : R) (ha : a ∈ y.asIdeal.primeCompl),
    IsUnit (M := Localization.AtPrime x.asIdeal)
      ((algebraMap R (Localization.AtPrime x.asIdeal) : (a : R) → Localization.AtPrime x.asIdeal)
          (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ y.asIdeal.primeCompl) a ha) : R) :
        Localization.AtPrime x.asIdeal)
⊢ IsUnit (M := Localization.AtPrime x.asIdeal)
    ((algebraMap R (Localization.AtPrime x.asIdeal) : (a : R) → Localization.AtPrime x.asIdeal)
        (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ y.asIdeal.primeCompl) a ha) : R) :
      Localization.AtPrime x.asIdeal)

Tactic:
rw [← PrimeSpectrum.le_iff_specializes, ← asIdeal_le_asIdeal, ← SetLike.coe_subset_coe, ←
        Set.compl_subset_compl] at h

Premises used: Set.compl_subset_compl, SetLike.coe_subset_coe, PrimeSpectrum.le_iff_specializes, PrimeSpectrum.asIdeal_le_asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x y : PrimeSpectrum R
h : (↑y.asIdeal : Set R)ᶜ ⊆ (↑x.asIdeal : Set R)ᶜ
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit (M := Localization.AtPrime x.asIdeal)
    ((algebraMap R (Localization.AtPrime x.asIdeal) : (a : R) → Localization.AtPrime x.asIdeal)
        (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ y.asIdeal.primeCompl) a ha) : R) :
      Localization.AtPrime x.asIdeal)

Tactic:
(IsLocalization.map_units (Localization.AtPrime x.asIdeal)
        ⟨a, show a ∈ x.asIdeal.primeCompl from h ha⟩ :)

Premises used: Localization.AtPrime, Subtype.mk, IsLocalization.map_units, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
x y : PrimeSpectrum R
h : (↑y.asIdeal : Set R)ᶜ ⊆ (↑x.asIdeal : Set R)ᶜ
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit (M := Localization.AtPrime x.asIdeal)
    ((algebraMap R (Localization.AtPrime x.asIdeal) : (a : R) → Localization.AtPrime x.asIdeal)
        (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ y.asIdeal.primeCompl) a ha) : R) :
      Localization.AtPrime x.asIdeal)

Tactic:
exact (IsLocalization.map_units (Localization.AtPrime x.asIdeal)
        ⟨a, show a ∈ x.asIdeal.primeCompl from h ha⟩ :)

Premises used: Localization.AtPrime, Subtype.mk, IsLocalization.map_units, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
Z : Set (PrimeSpectrum S)
hZ : IsClosed Z
hf : StableUnderSpecialization (comap f '' Z)
obtain :
  ∀ (I : Ideal S) (hZ : IsClosed (X := PrimeSpectrum S) (zeroLocus (↑I : Set S)))
    (hf : StableUnderSpecialization (comap f '' zeroLocus (↑I : Set S))), IsClosed (comap f '' zeroLocus (↑I : Set S))
⊢ IsClosed (comap f '' Z)

Tactic:
obtain ⟨I, rfl⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal Z).mp hZ

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus_ideal, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (X := PrimeSpectrum S) (zeroLocus (↑I : Set S))
hf : StableUnderSpecialization (comap f '' zeroLocus (↑I : Set S))
⊢ IsClosed (comap f '' zeroLocus (↑I : Set S))

Tactic:
(isClosed_iff_zeroLocus _).mpr ⟨I.comap f, le_antisymm ?_ fun p hp ↦ ?_⟩

Premises used: Iff.mpr, PrimeSpectrum.isClosed_iff_zeroLocus, le_antisymm, SetLike.coe, Ideal.comap, Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Topology
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (X := PrimeSpectrum S) (zeroLocus (↑I : Set S))
hf : StableUnderSpecialization (comap f '' zeroLocus (↑I : Set S))
refine_1 : comap f '' zeroLocus (↑I : Set S) ≤ zeroLocus (↑(Ideal.comap f I) : Set R)
refine_2 :
  ∀ (p : PrimeSpectrum R) (hp : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑(Ideal.comap f I) : Set R)) p),
    p ∈ comap f '' zeroLocus (↑I : Set S)
⊢ IsClosed (comap f '' zeroLocus (↑I : Set S))

Tactic:
refine (isClosed_iff_zeroLocus _).mpr ⟨I.comap f, le_antisymm ?_ fun p hp ↦ ?_⟩

Premises used: Iff.mpr, PrimeSpectrum.isClosed_iff_zeroLocus, le_antisymm, Exists.intro