Proving Ergodic in Mathlib: use Ergodic.of_preimage_eq with strict invariance

Mathlib's PreErgodic asks about sets that are invariant only a.e. (f ⁻¹' s =ᵐ[μ] s, null-measurable), which is awkward to verify directly. Ergodic.of_preimage_eq (hf : MeasurePreserving f μ μ) (h : ∀ s, MeasurableSet s → f ⁻¹' s = s → EventuallyEmptyOrUniv s (ae μ)) reduces to strictly invariant measurable sets. Close the goal with eventuallyEmptyOrUniv_iff: (∀ᵐ x, x ∈ s) ∨ (∀ᵐ x, x ∉ s). Example use: 'time averages converge to space averages for every integrable g' implies ergodicity, since for invariant s the Birkhoff averages of s.indicator 1 are constant in n ≥ 1, hence a.e. equal to μ.real s. Annotate s.indicator (1 : α → ℝ) explicitly, otherwise the numeral's type stays stuck.