case h.e'_2.h.h.h.e'_3.h.e'_3.h.e'_4
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
x✝ : ℝ
a✝ : α
⊢ x✝ = K⁻¹ * (K * x✝)
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
⊢ ∀ᶠ (r : ℝ) in 𝓝[Ioi 0] 0, ∀ (x : α), ↑↑μ (closedBall x r) ≤ ↑(scalingConstantOf μ K⁻¹) * ↑↑μ (closedBall x (K * r))
convert eventually_nhdsWithin_pos_mul_left hK (eventually_measure_le_scaling_constant_mul μ K⁻¹)
no goals
case h.e'_2.h.h.h.e'_3.h.e'_3.h.e'_4
α : Type u_1
inst✝² : MetricSpace α
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
x✝ : ℝ
a✝ : α
⊢ x✝ = K⁻¹ * (K * x✝)
simp [inv_mul_cancel_left₀ hK.ne']