case h
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr :
  ∀ (x : α) (t : ℝ),
    t ≤ K →
      ↑↑μ (closedBall x (t * r)) ≤
        ↑(Classical.choose
              (_ :
                ∃ C,
                  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                    ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
          ↑↑μ (closedBall x r)
x : α
⊢ ↑↑μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
⊢ ∀ᶠ (r : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
filter_upwards [Classical.choose_spec
    (exists_eventually_forall_measure_closedBall_le_mul μ K)]with r hr x
no goals
case h
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K r : ℝ
hr :
  ∀ (x : α) (t : ℝ),
    t ≤ K →
      ↑↑μ (closedBall x (t * r)) ≤
        ↑(Classical.choose
              (_ :
                ∃ C,
                  ∀ᶠ (ε : ℝ) in 𝓝[Ioi 0] 0,
                    ∀ (x : α) (t : ℝ), t ≤ K → ↑↑μ (closedBall x (t * ε)) ≤ ↑C * ↑↑μ (closedBall x ε))) *
          ↑↑μ (closedBall x r)
x : α
⊢ ↑↑μ (closedBall x (K * r)) ≤ ↑(scalingConstantOf μ K) * ↑↑μ (closedBall x r)
exact (hr x K le_rfl).trans (mul_le_mul_right' (ENNReal.coe_le_coe.2 (le_max_left _ _)) _)