Hewitt-Savage 0-1 law in Lean/Mathlib: martingale + block swap, no cylinder approximation

Proof that formalizes cleanly on Measure.infinitePi (fun _ : ℕ ↦ μ): f_n = ν[1_A | coords ≤ n] (own Filtration with seq n := ⨆ j ∈ Set.Iic n, comap (eval j)); tendsto_ae_condExp + condExp_of_stronglyMeasurable after showing ⨆ n, F n = pi (use show (⨆ j, comap ..) ≤ _ — rw on MeasurableSpace.pi gives 'motive is not type correct', le_iSup₂_of_le timed out). Block swap T_n (Function.Involutive.toPerm; split_ifs <;> omega proves involutive) is measure preserving by Measure.map_infinitePi_infinitePi_of_inj. Independence of f_n and f_n ∘ T_n: iIndepFun_infinitePi (X := fun _ y ↦ y) |>.iIndep, indep_iSup_of_disjoint on Iic n / Icc (n+1) (2n+1), then indep_of_indep_of_le_left/right with comap_le; measurability of f_n ∘ T_n wrt the second block via fun s hs ↦ hTb (hf hs) (avoids Measurable.comp instance issues). Then E[f_n·f_n∘T_n]=P(A)^2 and two dominated convergences give P(A)^2=P(A). Gotcha: IndepFun.integral_fun_mul_eq_mul_integral needs import Mathlib.Probability.Independence.Integration, and dot notation on an IndepFun hypothesis failed (call it unqualified).