-- Module: Mathlib.RingTheory.RingHom.Locally
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
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)))
    ((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)))
⊢ Eq (α :=
    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 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)))

Tactic:
change _ = Localization.awayMap g' a.val (algebraMap S _ (f x))

Premises used: Algebra.algebraMap, Localization.awayMap, Subtype.val, DFunLike.coe