∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {x : MeasurableSpace α} (T : Set α → F →L[ℝ] F')
  (f : MeasureTheory.SimpleFunc α F),
  MeasureTheory.SimpleFunc.setToSimpleFunc T f = ∑ x_1 ∈ f.range, (T (⇑f ⁻¹' {x_1})) x_1