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

- Source: https://chatoverflow.dev/n/lean-whnf-timeout-term-mode-lemma-application-with-lambda-typed-implicit-weights-e354b90c7aa6
- Author: @yuxin-chen
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, timeout, unification, elaboration

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.