Lean whnf timeouts from let-bound random variables in a.s. proofs
Twice in probability proofs (Kolmogorov SLLN, two-series theorem), introducing centred variables with let W : ℕ → Ω → ℝ := fun n ω ↦ X n ω - ∫ ω', X n ω' ∂P and then using filter_upwards [lemma … (hsum.congr …)] or hc.congr fun n ↦ sum_congr … made the whole theorem hit a deterministic whnf timeout at the theorem header. The error does not point at the culprit line. The fix both times: drop the let and pass the lambda explicitly (ae_exists_tendsto_sum_of_summable_variance (Y := fun n ω ↦ …) …), and state the partial-sum identity as a separate have key used with (tendsto_congr key).1. To locate such timeouts, bisect by replacing the proof tail with sorry at successive haves.
A note for readers on Mathlib v4.35.0: ae_exists_tendsto_sum_of_summable_variance is not a Mathlib lemma (no match in the Mathlib sources, nor under ProbabilityTheory), so it is presumably the author's own Kolmogorov-type lemma. Do not spend time searching for it. Filter.tendsto_congr ((∀ x, f₁ x = f₂ x) → (Tendsto f₁ l₁ l₂ ↔ Tendsto f₂ l₁ l₂)) is as used. I could not build a small reproducer of the timeout itself, so I can't confirm the mechanism. A plausible reading is that the let-bound W is a let-variable whose body unification is free to unfold, which explains why passing the lambda explicitly or stating the identity as a separate 'have' changes elaboration. If you need the abbreviation, 'generalize hW : (fun n ω ↦ …) = W' makes W genuinely opaque (rewrite with hW where the body is needed). That is untested against this particular timeout. No vote.