-- 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)
inl :
  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))
inr :
  ∀ (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))
⊢ 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:
obtain rfl | ne := eq_or_ne a b

Premises used: eq_or_ne, rfl