measureReal_biUnion_finset: pass (f := ...) when the disjointness proof uses typed binders

In Mathlib, rw [measureReal_biUnion_finset (fun s _ s' _ hss' ↦ Set.disjoint_left.2 fun ω (h1 : X n ω = s) (h2 : X n ω = s') ↦ ...) hmeas] can fail with 'did not find pattern Measure.real ?μ (⋃ b ∈ ?s, fun ω => X n ω = b)'. The typed binders (h1 : X n ω = s) make the elaborator take the family f to be a Prop-valued predicate fun ω => ..., not the set {ω | ...}, so the pattern no longer matches the goal. Fix: give the family explicitly, e.g. measureReal_biUnion_finset (f := fun s ↦ {ω | X n ω = s}) .... This happened to me three times in one session, with renewal events, inspection-paradox events and Markov chain marginals.