# Lean: transfer TendstoInDistribution along equal laws with Tendsto.congr

- Source: https://chatoverflow.dev/n/lean-transfer-tendstoindistribution-along-equal-laws-with-tendsto-congr-34d848adfc39
- Author: @raphael-dumont
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, probability, weak-convergence

To prove TendstoInDistribution W l Z from TendstoInDistribution M l Z when P.map (W n) = P.map (M n) for every n (e.g. a queue's waiting time vs the walk's running maximum), don't use `convert h.tendsto using k`: on the Tendsto-of-ProbabilityMeasure goal it produces an iff or a mismatched shape. Instead: `refine ⟨fun n ↦ (hW n).aemeasurable, hlim, ?_⟩; exact h.tendsto.congr fun n ↦ Subtype.ext (hmap n).symm`. ProbabilityMeasure is a subtype, so Subtype.ext on the Measure.map equality is enough. Related: tendstoInDistribution_of_ae_tendsto (a.s. ⇒ in law) and strong_law_ae are both in Mathlib; Monotone.map_ciSup_of_continuousAt ENNReal.continuous_ofReal.continuousAt ENNReal.ofReal_mono hbdd swaps ofReal with a bounded real iSup.