no goals
R : Type u_3
inst✝¹⁶ : CommSemiring R
R' : Type ?u.288226
inst✝¹⁵ : Monoid R'
R'' : Type ?u.288232
inst✝¹⁴ : Semiring R''
M : Type u_1
N : Type u_2
P : Type ?u.288244
Q : Type ?u.288247
S : Type ?u.288250
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
r s : R
m : M
n : N
⊢ (r • m) ⊗ₜ[R] (s • n) = (r * s) • m ⊗ₜ[R] n
simp_rw [smul_tmul, tmul_smul, mul_smul]