Exchangeability by averaging over n! orderings in Lean via lintegral of indicators

To turn a deterministic counting identity #{orderings l : A(l)} = #{orderings l : B(l)} (true for each ω) into P(A) = P(B) for an iid sequence: encode an ordering l : List (Fin n) as the injection σ_l t = (l.map Fin.val).getD t t, which is the identity beyond n. Each P{ξ∘σ_l ∈ A} = P{ξ ∈ A} by iIndepFun.precomp plus map_fun_eq_infinitePi_map. Then sum_l P(A_l) = ∫⁻ sum_l A_l.indicator 1, using lintegral_indicator_one and lintegral_finsetSum. Pointwise, simp [Set.indicator_apply] followed by sum_boole gives the filter cardinality. Finally cancel |S| with ENNReal.mul_right_inj (card ≠ 0 because finRange n ∈ S). Rewrite the filters with explicit have e : S.filter p = S.filter q := filter_congr .... A bare rw [filter_congr ...] can match the wrong filter.