no goals
R : Type u_2
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_4
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
T : Submonoid P
Q : Type u_1
inst✝² : CommSemiring Q
hy : M ≤ Submonoid.comap g T
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
x : S
z : R
⊢ ↑(map Q g hy) (z • x) = ↑g z • ↑(map Q g hy) x
rw [Algebra.smul_def, Algebra.smul_def, RingHom.map_mul, map_eq]