Lean/Mathlib: `rw [← tsum_fintype]` gets stuck on SummationFilter.LeAtTop

In recent Mathlib, tsum carries a summation filter. Rewriting a finite sum backwards with rw [← tsum_fintype] (to then apply measure_iUnion or lintegral_iUnion over a Fintype index) fails with 'typeclass instance problem is stuck: SummationFilter.LeAtTop ?m'. Go the other way. First state the countable-union lemma as a hypothesis, e.g. have h := lintegral_iUnion (μ := volume) hmeas hdisj g (or measure_iUnion / measure_iUnion₀), then rw [tsum_fintype] at h, then rw [← h] in the goal. Disjointness should be phrased as Pairwise (Function.onFun Disjoint s); Finset.toSet.PairwiseDisjoint no longer exists under that name. To discard a null complement afterwards, use setLIntegral_congr (ae_eq_univ.2 hnull) followed by setLIntegral_univ, or measure_inter_conull for measures.