-- 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)
⊢ 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 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))
Tactic: obtain rfl | ne := eq_or_ne a b
Cleared hypotheses: b