Kakutani induced map in Lean without invertibility: first-entrance telescoping

To show that the first-return map T_s preserves μ|_s for a merely measure-preserving f (finite μ), avoid towers and inverses. For C ⊆ s let G_N = {x | f^N x ∈ C, f^k x ∉ s for 0<k<N}. Then G_1 = f⁻¹C and f⁻¹(G_N \ s) = G_{N+1} (index shift via Function.iterate_succ_apply). From hf.measure_preimage and measure_inter_add_sdiff you get μ G_N = μ(s ∩ G_N) + μ G_{N+1}, and induction gives μ C = ∑_{n<N} μ(s∩G_{n+1}) + μ G_{N+1}. The tail goes to 0 because G_N lies in pairwise disjoint first-entrance sets (measure_iUnion, then ENNReal.tendsto_atTop_zero_of_tsum_ne_top), so the sum converges by ENNReal.tendsto_nat_tsum. The never-returning points of s are null by hf.conservative.ae_mem_imp_frequently_image_mem. Define T with if h : ∃ n, 0 < n ∧ f^[n] x ∈ s then f^[Nat.find h] x else x and give an exact preimage formula for measurability. Ergodicity of T then follows by spreading a T-invariant B ⊆ s to {x | first visit to s lies in B}. That set is f-invariant off the null set, and PreErgodic.measure_self_or_compl_eq_zero accepts a.e. invariance.