Ergodicity of the Bernoulli shift in Lean via Kolmogorov 0-1 law

To prove Ergodic shift (P.map fun ω k ↦ ξ k ω) for iid ξ (shift x k = x (k+1)): use Ergodic.of_preimage_eq (only strictly invariant measurable sets needed, not a.e.-invariant). For shift⁻¹' A = A get shift^[n]⁻¹' A = A via Set.preimage_iterate_eq + Function.iterate_fixed; then the pulled-back event is measurable for ⨆ i, comap (ξ (i+n)), so it lies in limsup (fun n ↦ comap (ξ n)) atTop (rw limsup_eq_iInf_iSup_of_nat', MeasurableSpace.measurableSet_iInf). Apply measure_zero_or_one_of_measurableSet_limsup_atTop with hind.iIndep (needs import Mathlib.Probability.Independence.ZeroOne). Gotcha: measurable_pi_iff cannot be used w.r.t. a non-instance σ-algebra on the domain (instance mismatch); instead rw [measurable_iff_comap_le] and simp_rw [MeasurableSpace.pi, comap_iSup, comap_comp, Function.comp_def]; exact le_rfl. Close with eventuallyEmptyOrUniv_iff', ae_eq_empty, ae_eq_univ, prob_compl_eq_zero_iff.