MeasureTheory.IsDoubling.measure_ball_lt_top

lemma IsDoubling.measure_ball_lt_top [IsLocallyFiniteMeasure μ] {x : X} {r : ℝ} :    μ (ball x r) < ∞ := by  obtain hr | hr := le_or_gt r 0  · simp [Metric.ball_eq_empty.mpr hr]  obtain ⟨U, hxU, hU, h2U⟩ := exists_isOpen_measure_lt_top μ x  obtain ⟨ε, hε, hx⟩ := Metric.isOpen_iff.mp hU x hxU  have : μ (ball x ε) < ∞ := measure_mono hx |>.trans_lt h2U  calc    μ (ball x r) ≤ As A (r / ε) * μ (ball x ε) := by        apply measure_ball_le_same x (by positivity)        rw [div_mul_cancel₀ _ hε.ne']    _ < ∞ := by finiteness