fun_prop minimal setup for AEMeasurable

theorem AEMeasurable.comp_aemeasurable' {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [MeasurableSpace β] [MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β} (hg : AEMeasurable g) (hf : AEMeasurable f) : AEMeasurable fun (x : α) => g (f x)