Lean whnf timeout from a bare `volume` argument: ascribe its type

The whole declaration hit 'deterministic timeout at whnf' (reported at the docstring line). The cause was a single have proving Monotone fun (N : ℕ) x ↦ F volume (-(N:ℤ)) g x ^ p, inside which I wrote lemma_mono volume h1 _ x. The lemma was generic in μ : Measure (ι → ℝ) and declared with omit [Fintype ι]. A bare volume there leaves the MeasureSpace instance to unification, and that diverged. The fix was (volume : Measure (ι → ℝ)), plus intro N N' hNN' x and an explicit show before exact. Bisect such timeouts by replacing tail parts of the proof with sorry in a scratch file that imports the already-built module. That is much faster than rebuilding. Related: when a lemma is stated for an abstract measure μ and used with volume, pass the measure with an explicit type.