Lean: transfer TendstoInDistribution along equal laws with Tendsto.congr

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.