awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
i : ι
⊢ IsOpenMap (Y := PrimeSpectrum ((i : ι) → R i)) fun (a : PrimeSpectrum (R i)) ↦
    sigmaToPi R (Sigma.mk (β := fun (i : ι) ↦ PrimeSpectrum (R i)) i a)
have 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)
Tactic: simp only [sigmaToPi_apply, PrimeSpectrum.isTopologicalBasis_basic_opens.isOpenMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
i : ι
f : 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)
have refine_3 : IsOpen (↑(basicOpen (Pi.single (M := R) i f)) : Set (PrimeSpectrum ((i : ι) → R i)))
Tactic: rw [PrimeSpectrum.comap_evalRingHom_basicOpen]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
have refine_1 : Continuous (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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommRing (R i)
refine_1 : Continuous (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
have refine_2 : Function.Injective (α := (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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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)
⊢ IsOpenEmbedding (X := (i : ι) × PrimeSpectrum (R i)) (sigmaToPi R)
have refine_3 : IsOpenMap (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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
x : PiLocalization R
⊢ ∃ (a : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x
have this : ∀ (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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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}
⊢ ∃ (a : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x
have 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
Tactic: choose f hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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 (f ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a)) (Localization.Away (↑a : R))
have simp_rw : IsLocalization.Away (↑a : R) (Localization.Away (↑a : R))
Tactic: simp_rw [e, Equiv.apply_ofInjective_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
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 : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x
have 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))
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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
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))
⊢ ∃ (a : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x
have span_eq : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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)
⊢ (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
    singleton (α := PrimeSpectrum R) ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a : PrimeSpectrum R)
have simp_rw₁ : (↑(basicOpen (↑a : R)) : Set (PrimeSpectrum R)) =
  (↑(basicOpen (f (((Equiv.ofInjective f sorry).symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R) a))) :
    Set (PrimeSpectrum R))
Tactic: simp_rw [e, ← hf, Equiv.apply_ofInjective_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
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 : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x
have 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)
Tactic: replace hf a : (basicOpen a.1 : Set _) = {e.symm a} := by
    simp_rw [e, ← hf, Equiv.apply_ofInjective_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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
⊢ Eq (α := TopologicalSpace.Opens (PrimeSpectrum R)) (basicOpen ((↑a : R) * (↑b : R))) ⊥
have 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))
Tactic: simp_rw [basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf, hf]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
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
⊢ 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))
have nil : 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))
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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 : R), (toPiLocalization R : (a : R) → PiLocalization R) a = x
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
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
have refine : ∀ (I : PrimeSpectrum R), (toPiLocalization R : (a : R) → PiLocalization R) r I = x I
Tactic: refine ⟨r, funext fun I ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (hypothesis)
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
⊢ (toPiLocalization R : (a : R) → PiLocalization R) r I = x I
have this : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : DiscreteTopology.{u} (PrimeSpectrum R)
⊢ Function.Surjective (α := R) (β := MaximalSpectrum.PiLocalization R)
    (⇑(MaximalSpectrum.toPiLocalization R) : (a : R) → MaximalSpectrum.PiLocalization R)
have rw : Function.Surjective (α := R) (β := MaximalSpectrum.PiLocalization R)
  (⇑(AlgHom.comp (piLocalizationToMaximal R) (toPiLocalization R)) : (a : R) → MaximalSpectrum.PiLocalization R)
Tactic: rw [← piLocalizationToMaximal_comp_toPiLocalization]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Topology (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : PrimeSpectrum R
⊢ x ≤ y ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (closure {x}) y
have rw : x.asIdeal ≤ y.asIdeal ↔ 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]