∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {Rₘ : Type u_4} (Sₙ : Type u_5) (Rₘ' : Type u_6) (Sₙ' : Type u_7) [inst_3 : CommSemiring Rₘ]
  [inst_4 : CommSemiring Sₙ] [inst_5 : CommSemiring Rₘ'] [inst_6 : CommSemiring Sₙ'] [inst_7 : Algebra R Rₘ]
  [inst_8 : Algebra S Sₙ] [inst_9 : Algebra R Rₘ'] [inst_10 : Algebra S Sₙ'] [inst_11 : Algebra R Sₙ]
  [inst_12 : Algebra Rₘ Sₙ] [inst_13 : Algebra Rₘ' Sₙ'] [inst_14 : Algebra R Sₙ'] (N : Submonoid S)
  [inst_15 : IsLocalization M Rₘ] [inst_16 : IsLocalization N Sₙ] [inst_17 : IsLocalization M Rₘ']
  [inst_18 : IsLocalization N Sₙ'] [IsScalarTower R Rₘ Sₙ] [IsScalarTower R S Sₙ] [IsScalarTower R Rₘ' Sₙ']
  [IsScalarTower R S Sₙ'] (x : Rₘ),
  ((↑(IsLocalization.algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ)) x =
    ((algebraMap Rₘ' Sₙ').comp ↑(IsLocalization.algEquiv M Rₘ Rₘ')) x