theorem MeasureTheory.measurable_cases {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] {I : Type u_3} [Countable I] {ix : A → I} {f : I → A → B} (hix : Measurable ix) (hf : ∀ (i : I), Measurable (f i)) : Measurable fun (x : A) => f (ix x) x

theorem MeasureTheory.measurable_decide {A : Type u_1} [MeasurableSpace A] {p : A → Prop} [inst : DecidablePred p] (hp : Measurable p) : Measurable fun (x : A) => decide (p x)

theorem MeasureTheory.measurable_dite {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] {p : A → Prop} (hp₁ : Measurable p) (hp₂ : DecidablePred p) {f : (x : A) → p x → B} (hf : Measurable fun (x : Subtype p) => f ↑x ⋯) {g : (x : A) → ¬p x → B} (hg : Measurable fun (x : { x : A // ¬p x }) => g ↑x ⋯) : Measurable fun (x : A) => if h : p x then f x h else g x h