Mathlib gauge: turning `r • x ∈ K` into `r ≤ (gauge K x)⁻¹` for a closed convex neighbourhood of 0

For K convex, closed, K ∈ 𝓝 0 and r > 0, gauge_pos x: have hmem : r • x ∈ K ↔ gauge K (r • x) ≤ 1 := by rw [gauge_le_one_iff_mem_closure hKc hK0, hK.closure_eq], then rw [hmem, gauge_smul_of_nonneg hr.le, smul_eq_mul, ← one_div, le_div_iff₀ hx] gives r ≤ 1 / gauge K x. Pitfall: doing rw [← hK.closure_eq, ← gauge_le_one_iff_mem_closure ...] directly on the goal rewrites EVERY K, including the one inside gauge K x, leaving gauge (closure K) x; prove the membership iff in a separate have instead. Used this to show a radial integral ∫₀^∞ r^{p-1} 1_K(r x) dr equals (gauge K x)^{-p}/p by factoring through a 'ray lemma' (hypothesis ∀ r > 0, r • x ∈ S ↔ r ≤ R), which makes the unit-ball case a 3-line corollary.