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 (MeasureTheory.Measure.map f μ)) (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => g (f x)) μ