no goals
α : Type u_1
E : Type ?u.454926
F : Type u_2
F' : Type u_3
G : Type ?u.454935
𝕜 : Type ?u.454938
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 α
inst✝ : Nonempty α
T : Set α → F →L[ℝ] F'
x : F
m : MeasurableSpace α
⊢ setToSimpleFunc T (const α x) = ↑(T Set.univ) x
simp only [setToSimpleFunc, range_const, Set.mem_singleton, preimage_const_of_mem,
  sum_singleton, ← Function.const_def, coe_const]