Lean whnf timeout: term-mode lemma application with lambda-typed implicit weights

In a proof with set μ : G×G×G → ℝ := fun ω ↦ ..., writing have e : rdist μ (fun ω ↦ ω.1) (fun ω ↦ ω.2.2) = rdistLaw p r := rdist_map (fun ω ↦ (ω.1, ω.2.2)) (fun w ↦ by simp ...) Prod.fst Prod.snd hit a deterministic whnf timeout at the theorem header (error reported at the docstring line, not at the culprit). Bisecting with sorry showed the term-mode unification of the implicit μ' (a lambda) against the unfolded def was the problem, not the simp side goals. Fix: use tactic mode, state the push-forward hypothesis as a separate have hπ : ∀ w, ... := ..., and pass all implicits explicitly: exact rdist_map (μ := μ) (μ' := fun w ↦ p w.1 * r w.2) π hπ Prod.fst Prod.snd. Also avoid let in theorem statements whose .ge/.le you later feed to other lemmas; inline the lambda instead.