R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_4
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type ?u.3264412
inst✝⁹ : CommRing P
Rₘ : Type u_3
Sₘ : Type u_2
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : { x // x ∈ M }
⊢ ↑(algebraMap Rₘ Sₘ) (mk' Rₘ (↑y * x) y) = ↑(algebraMap Rₘ Sₘ) (↑(algebraMap R Rₘ) x)
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_4
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type ?u.3264412
inst✝⁹ : CommRing P
Rₘ : Type u_3
Sₘ : Type u_2
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : { x // x ∈ M }
⊢ ↑(algebraMap Rₘ Sₘ) (mk' Rₘ x y) =
    mk' Sₘ (↑(algebraMap R S) x)
      { val := ↑(algebraMap R S) ↑y, property := (_ : ↑(algebraMap R S) ↑y ∈ Algebra.algebraMapSubmonoid S M) }
rw [IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, ←
  IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R Rₘ Sₘ,
  IsScalarTower.algebraMap_apply R Rₘ Sₘ, ← _root_.map_mul, mul_comm,
  IsLocalization.mul_mk'_eq_mk'_of_mul]
no goals
R : Type u_1
inst✝¹² : CommRing R
M : Submonoid R
S : Type u_4
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
P : Type ?u.3264412
inst✝⁹ : CommRing P
Rₘ : Type u_3
Sₘ : Type u_2
inst✝⁸ : CommRing Rₘ
inst✝⁷ : CommRing Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : IsLocalization M Rₘ
inst✝⁴ : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst✝³ : Algebra Rₘ Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R Rₘ Sₘ
inst✝ : IsScalarTower R S Sₘ
x : R
y : { x // x ∈ M }
⊢ ↑(algebraMap Rₘ Sₘ) (mk' Rₘ (↑y * x) y) = ↑(algebraMap Rₘ Sₘ) (↑(algebraMap R Rₘ) x)
exact congr_arg (algebraMap Rₘ Sₘ) (IsLocalization.mk'_mul_cancel_left x y)