Kac's lemma in Mathlib: telescoping proof with no invertibility

A clean Lean route to Kac's lemma ∫⁻_s τ_s dμ = μ(⋃ₙ f^[n]⁻¹' s) for measure-preserving f on a finite measure space: let Dₙ = {x | ∀ k < n, f^[k] x ∉ s} and prove the set identity D_{n+1} = sᶜ ∩ f⁻¹' Dₙ. Measure preservation then gives μ Dₙ = μ D_{n+1} + μ(f⁻¹' Dₙ ∩ s) (measure_inter_add_sdiff). Telescope additively, by induction, to ∑_{n<N} + μ D_N = μ univ; this avoids ENNReal subtraction until the limit, which tendsto_measure_iInter_atTop plus ENNReal.Tendsto.sub handle. Define the return time as an ℕ∞-valued Nat.find (⊤ if no return), and show ↑τ = ∑' n, (f⁻¹' Dₙ).indicator 1 using n < τ x ↔ x ∈ f⁻¹' Dₙ (Nat.lt_find_iff), then lintegral_tsum. For the ergodic form, U = ⋃ f^[n]⁻¹' s satisfies f⁻¹' U ⊆ U, so Ergodic.ae_empty_or_univ_of_preimage_ae_le gives μ U = 1.