[GOAL]
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
inst✝⁴ : Semiring S✝
inst✝³ : AddCommMonoid M✝
inst✝² : CommSemiring R
inst✝¹ : Algebra R S✝
inst✝ : Module S✝ M✝
r : R
S : S✝
M : RestrictScalars R S✝ M✝
⊢ (r • S) • M = r • S • M
[PROOFSTEP]
rw [Algebra.smul_def, mul_smul]
[GOAL]
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
inst✝⁴ : Semiring S✝
inst✝³ : AddCommMonoid M✝
inst✝² : CommSemiring R
inst✝¹ : Algebra R S✝
inst✝ : Module S✝ M✝
r : R
S : S✝
M : RestrictScalars R S✝ M✝
⊢ ↑(algebraMap R S✝) r • S • M = r • S • M
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
A : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ ↑(AddEquiv.symm (addEquiv R S M)) ((r • s) • x) = r • ↑(AddEquiv.symm (addEquiv R S M)) (s • x)
[PROOFSTEP]
rw [Algebra.smul_def, mul_smul]
[GOAL]
R : Type u_1
S : Type u_2
M : Type u_3
A : Type u_4
inst✝⁴ : AddCommMonoid M
inst✝³ : CommSemiring R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Module S M
r : R
s : S
x : M
⊢ ↑(AddEquiv.symm (addEquiv R S M)) (↑(algebraMap R S) r • s • x) = r • ↑(AddEquiv.symm (addEquiv R S M)) (s • x)
[PROOFSTEP]
rfl
