∀ {α : Type u_5} {γ : Type u_6} [inst : MeasurableSpace α] [Nonempty γ] {P : MeasureTheory.SimpleFunc α γ → Prop},
  (∀ (c : γ), P (MeasureTheory.SimpleFunc.const α c)) →
    (∀ ⦃f g : MeasureTheory.SimpleFunc α γ⦄ {s : Set α} (hs : MeasurableSet s),
        P f → P g → P (MeasureTheory.SimpleFunc.piecewise s hs f g)) →
      ∀ (f : MeasureTheory.SimpleFunc α γ), P f