-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
x : R
⊢ Eq (α :=
    Localization.Away (M := Localization.Away (↑b : T))
      ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T)))
    ((algebraMap T
            (Localization.Away (M := Localization.Away (↑b : T))
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                  ((g : (a : S) → T) (↑a : S)) :
                Localization.Away (↑b : T))) :
          (a_1 : T) →
            Localization.Away
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                ((g : (a : S) → T) (↑a : S))))
        ((g : (a : S) → T) ((f : (a : R) → S) x : S)) :
      Localization.Away (M := Localization.Away (↑b : T))
        ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
            ((g : (a : S) → T) (↑a : S)) :
          Localization.Away (↑b : T)))
    ((Localization.awayMap g' (↑a : S) :
          (a_1 : Localization.Away (↑a : S)) → Localization.Away ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S)))
        ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) x)) :
      Localization.Away (M := Localization.Away (↑b : T))
        ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T)))
have a₁ : Eq (α :=
  Localization.Away (M := Localization.Away (↑b : T))
    ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T)))
  ((algebraMap T
          (Localization.Away (M := Localization.Away (↑b : T))
            ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                ((g : (a : S) → T) (↑a : S)) :
              Localization.Away (↑b : T))) :
        (a_1 : T) →
          Localization.Away
            ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
              ((g : (a : S) → T) (↑a : S))))
      ((g : (a : S) → T) ((f : (a : R) → S) x : S)) :
    Localization.Away (M := Localization.Away (↑b : T))
      ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
        Localization.Away (↑b : T)))
  ((algebraMap (Localization.Away (↑b : T))
          (Localization.Away (M := Localization.Away (↑b : T))
            ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T))) :
        (a_1 : Localization.Away (↑b : T)) → Localization.Away ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S)))
      ((g' : (a : S) → Localization.Away (↑b : T)) ((f : (a : R) → S) x)) :
    Localization.Away (M := Localization.Away (↑b : T))
      ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T)))
Tactic: simp only [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_eq]