∀ {α : Type u_1} {E : Type u_2} {F' : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T T' : Set α → E →L[ℝ] F') (c : ℝ),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) →
    ∀ {f : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        MeasureTheory.SimpleFunc.setToSimpleFunc T' f = c • MeasureTheory.SimpleFunc.setToSimpleFunc T f