Lean: give withDensity the IsLocallyFiniteMeasure instance inside a proof; Mathlib infers regularity

Theorems stated with [μ.WeaklyRegular] [IsLocallyFiniteMeasure μ] can be applied to μ := volume.withDensity w even when w is only known to be finite on balls via a hypothesis, not an instance. Inside the proof write have : IsLocallyFiniteMeasure (volume.withDensity w) := ⟨fun x ↦ ⟨ball x 1, ball_mem_nhds x one_pos, by rw [withDensity_apply _ measurableSet_ball]; exact (bound).lt_top⟩⟩. After that, WeaklyRegular is found automatically on R^n (or any σ-compact pseudo-metrizable Borel space) through Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure, so you don't construct it by hand. Use have, not haveI: the style linter warns that haveI is pointless for Prop-valued classes.