-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hT_1 :
  ∀ (r : (↑s : Type u)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra S T) (_ : IsLocalization.Away (↑r : S) T),
      P (comp (algebraMap S T) f)
r : (↑s : Type u)
T : Type u
w : CommRing T
w_1 : Algebra S T
w_2 : IsLocalization.Away (↑r : S) T
hT : P (comp (algebraMap S T) f)
h :
  Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (comp
        (@comp _ _ _ _ Semiring.toNonAssocSemiring _
          (RingEquiv.toRingHom
            (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
          (algebraMap S T))
        f :
      R →+* Localization (Submonoid.powers (↑r : S)))
h₁ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
h₂ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (↑(AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T)) :
          T →+* Localization (Submonoid.powers (↑r : S)))
        (algebraMap S T))
      f)
h₃ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp
      (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map (M := Submonoid.powers (↑r : S)) (T := Submonoid.powers (↑r : S))
          (Localization (Submonoid.powers (↑r : S))) (id S) ⋯)
        (algebraMap S T))
      f)
h₄ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp (comp (algebraMap S (Localization (Submonoid.powers (↑r : S)))) (id S)) f)
h₅ h₆ :
  Eq (α := R →+* Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
    (comp (algebraMap S (Localization (Submonoid.powers (↑r : S)))) f)
⊢ Eq (α := R →+* Localization.Away (↑r : S))
    (comp (algebraMap S (Localization.Away (↑r : S))) f : R →+* Localization.Away (↑r : S))
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _
        (RingEquiv.toRingHom
          (AlgEquiv.toRingEquiv (AlgEquiv.symm (Localization.algEquiv (Submonoid.powers (↑r : S)) T))))
        (comp (algebraMap S T) f) :
      R →+* Localization (Submonoid.powers (↑r : S)))

Tactic:
rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe,
    AlgEquiv.toRingEquiv_toRingHom, Localization.coe_algEquiv_symm, IsLocalization.map_comp,
    RingHom.comp_id]

Premises used: AlgEquiv.toRingEquiv_toRingHom, IsLocalization.map_comp, RingHom.comp_assoc, RingHom.comp_id, RingEquiv.toRingHom_eq_coe, Localization.coe_algEquiv_symm