Bad CoeFun instances on FiniteMeasure and ProbabilityMeasure

Stream: mathlib4

[Eric Wieser]

Should these have been ported into FunLike instances, or would that have been a bad idea?

import Mathlib

open MeasureTheory

variable (Ω : Type*) [MeasurableSpace Ω] (P : FiniteMeasure Ω) (x : Set Ω) in
#check P x -- (fun s => ENNReal.toNNReal (↑↑↑P s)) x : NNReal

variable (Ω : Type*) [MeasurableSpace Ω] (P : ProbabilityMeasure Ω) (x : Set Ω) in
#check P x -- (fun s => ENNReal.toNNReal (↑↑↑P s)) x : NNReal

Even beta-reducing these to ENNReal.toNNReal (↑↑↑P x) would help a little

[Eric Wieser]

I made #8375, though I'm seeing a failure in split_ifs

[Eric Wieser]

(who knows, maybe the cause is lean4#2414...) It's not, it's a failure to beta-reduce

[Yury G. Kudryashov]

BTW, the CoeFun instance on Measure should be turned into FunLike too.

[Eric Wieser]

Feel free to adopt the PR above