no goals
α : Type u_1
E : Type ?u.241077
F : Type u_2
F' : Type u_3
G : Type ?u.241086
𝕜 : Type ?u.241089
p : ℝ≥0∞
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m✝ : MeasurableSpace α
μ : Measure α
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
c : ℝ
f : α →ₛ F
⊢ setToSimpleFunc (fun s => c • T s) f = c • setToSimpleFunc T f
simp_rw [setToSimpleFunc, ContinuousLinearMap.smul_apply, smul_sum]