-- 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))
I : PrimeSpectrum R
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))
rwa :
  ∀
    (this :
      Eq (α :=
        Localization.AtPrime (R := R)
          (asIdeal
            ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
              ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I))))
        ((AlgEquiv.symm (algE ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)) :
              (a : Localization.Away (↑((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I) : R)) →
                Localization.AtPrime
                  ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
                      ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)).asIdeal)
            ((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.AtPrime (R := R)
            (asIdeal
              ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
                ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I))))
        (x
            ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
              ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)) :
          Localization (M := R)
            (Ideal.primeCompl
              (asIdeal
                ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
                  ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)))))),
    (toPiLocalization R : (a : R) → PiLocalization R) r I = x I
⊢ (toPiLocalization R : (a : R) → PiLocalization R) r I = x I
have rwa₁ : ∀
  (this :
    Eq (α :=
      Localization.AtPrime (R := R)
        (asIdeal
          ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
            ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I))))
      ((algebraMap R
              (Localization.AtPrime (R := R)
                (asIdeal
                  ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
                    ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)))) :
            (a : R) →
              Localization.AtPrime
                ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
                    ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)).asIdeal)
          r :
        Localization.AtPrime (R := R)
          (asIdeal
            ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
              ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I))))
      (x
          ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
            ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)) :
        Localization (M := R)
          (Ideal.primeCompl
            (asIdeal
              ((e.symm : (a : (↑(Set.range f) : Type u)) → PrimeSpectrum R)
                ((e : (a : PrimeSpectrum R) → (↑(Set.range f) : Type u)) I)))))),
  (toPiLocalization R : (a : R) → PiLocalization R) r I = x I
Tactic: rwa [← AlgEquiv.symm_apply_eq, AlgEquiv.commutes, e.symm_apply_apply] at this
Cleared hypotheses: this