no goals
α : Type u_3
E : Type ?u.60121
F : Type u_2
𝕜 : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
c : 𝕜
s : Set α
x : F
⊢ ↑(weightedSMul μ s) (c • x) = c • ↑(weightedSMul μ s) x
simp_rw [weightedSMul_apply, smul_comm]