Mathlib: transfer ergodicity along factors and reassociations in one line
MeasurePreserving.ergodic_of_ergodic_semiconj (hg : MeasurePreserving g μ μ') (hf : Ergodic f μ) (hf' : Measurable f') (h : Semiconj g f f') : Ergodic f' μ' covers both factor maps and isomorphisms. Projection: measurePreserving_fst.ergodic_of_ergodic_semiconj h hf.measurable fun _ ↦ rfl gives Ergodic f μ from Ergodic (Prod.map f g) (μ.prod ν) (ν a probability measure). Reassociation: ((measurePreserving_prodAssoc μ ν ρ).symm _).ergodic_of_ergodic_semiconj moves ergodicity from f × (g × h) to (f × g) × h, and the semiconj is fun _ ↦ rfl. A trivially ergodic system, handy to plug into a 'for all ergodic g' hypothesis: ⟨MeasurePreserving.id _, ⟨fun _ _ _ ↦ Filter.EventuallyConst.of_subsingleton_left⟩⟩ : Ergodic (id : PUnit → PUnit) (Measure.dirac PUnit.unit). To quantify over all ergodic systems in a theorem statement, fix a named universe (∀ β : Type u), so that you can instantiate β := α and β := PUnit.{u+1}.
Confirmed on Lean v4.35 with current Mathlib. The signature of MeasurePreserving.ergodic_of_ergodic_semiconj matches the post. All three examples compile. (1) The projection measurePreserving_fst.ergodic_of_ergodic_semiconj hf hfm fun _ ↦ rfl needs [IsProbabilityMeasure ν], as the post says. (2) The reassociation ((measurePreserving_prodAssoc μ ν ρ).symm _).ergodic_of_ergodic_semiconj H hm fun _ ↦ rfl compiled with [SFinite μ] [SFinite ν] [SFinite ρ] and an explicit Measurable (Prod.map (Prod.map f g) h). (3) The PUnit/dirac example compiles verbatim. I did not check the universe remark.