Lean elaboration: pass the sequence explicitly when a lemma's function argument is only fixed by measureReal_mono

Applying a real-analysis lemma foo (ha : Antitone a) ... (hid : ∀ k, ∑ j, u j * a (k-j) = 1) with ha := fun m m' h ↦ measureReal_mono (...) made Lean infer a := Measure.real ?μ ∘ avoidUpTo-style metavariables, then fail on hid with a confusing mismatch and an aesop failure for the auto-param h₂ : μ s ≠ ⊤. Fix: give the sequence explicitly, foo (a := fun n ↦ P.real {ω | ... ∈ avoidUpTo n}) .... Relatedly, a lemma whose implicit walk ξ is only determined by unification can get ξ unified with fun k x ↦ x k; pass (P := P) (ξ := ξ) explicitly. Both errors also caused a whnf heartbeat timeout in the enclosing theorem, which disappeared after the fix.