-- Lean 4 proof step from Mathlib.RingTheory.Extension.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
M : Submonoid S
S' : Type u_1
inst_3 : CommRing S'
inst_4 : Algebra S S'
inst_5 : IsLocalization M S'
inst_6 : Algebra R S'
inst_7 : IsScalarTower R S S'
P : Extension.{w, u, v} R S
this : Algebra.{w, u_1} (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S' :=
  RingHom.toAlgebra
    (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
      (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
h :
  Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))
      _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
        (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
      (algebraMap R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
h₁ :
  Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))
      _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
        (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
      (@RingHom.comp _ P.Ring _ _ Semiring.toNonAssocSemiring _
        (algebraMap P.Ring (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)))
        (algebraMap R P.Ring)))
h₂ :
  Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ P.Ring _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) _ _
        Semiring.toNonAssocSemiring _
        (IsLocalization.lift (R := P.Ring) (M := Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)
          (g := @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S)) ⋯)
        (algebraMap P.Ring (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
      (algebraMap R P.Ring))
h₃ :
  Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ P.Ring _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
      (algebraMap R P.Ring))
h₄ :
  Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S')
      (@RingHom.comp.{u, w, v} _ P.Ring _ _ Semiring.toNonAssocSemiring _ (algebraMap P.Ring S) (algebraMap R P.Ring)))
⊢ Eq (α := R →+* S') (algebraMap R S')
    (@RingHom.comp.{u, w, u_1} _ (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))
      _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M)) S')
      (algebraMap R (Localization (Submonoid.comap (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S) M))))
have h₅ : Eq (α := R →+* S') (algebraMap R S')
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap R S))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_eq R P.Ring (Localization _),
      ← RingHom.comp_assoc, IsLocalization.lift_comp, RingHom.comp_assoc,
      ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]