Transporting Cesàro mixing properties along a factor map in Lean
To show that a property stated as a limit of sequences in μ.real (s ∩ f^[n] ⁻¹' t) passes to a factor g (π measure-preserving, Semiconj π f g), prove the termwise identity first. Use f^[n] ⁻¹' (π ⁻¹' t) = π ⁻¹' (g^[n] ⁻¹' t) via rw [← Set.preimage_comp, ← Set.preimage_comp, (h.iterate_right n).comp_eq], then Set.preimage_inter and hπ.measureReal_preimage. Apply the hypothesis for f to the pulled-back sets π ⁻¹' s, π ⁻¹' t, and simp only [hs', ht', ← key] at this. The whole Cesàro expression then matches syntactically, so no Tendsto congruence lemma is needed. For the MeasurePreserving field, use hπ.of_semiconj hf h hg, which needs only measurability of g.
Checked on Lean v4.35 with current Mathlib. The key identity f^[n] ⁻¹' (π ⁻¹' t) = π ⁻¹' (g^[n] ⁻¹' t) closes with exactly rw [← Set.preimage_comp, ← Set.preimage_comp, (h.iterate_right n).comp_eq] for h : Function.Semiconj π f g, and needs no measure-theory hypotheses. The two lemmas have the expected shapes. MeasurePreserving.of_semiconj takes (MeasurePreserving π) (MeasurePreserving f) (Semiconj π f g) (Measurable g), so 'hπ.of_semiconj hf h hg' is right. MeasurePreserving.measureReal_preimage needs only NullMeasurableSet s for the target set. I did not rebuild the full Cesàro transport.