MeasureTheory.isOpenPosMeasure_of_isDoubling

lemma isOpenPosMeasure_of_isDoubling [NeZero μ] : IsOpenPosMeasure μ := by  refine ⟨fun U hU ⟨x, hx⟩ h3U ↦ ?_⟩  obtain ⟨r, hr, hx⟩ := Metric.isOpen_iff.mp hU x hx  obtain ⟨r', h⟩ : ∃ r', μ (ball x r') ≠ 0 := by    have hμ := NeZero.ne μ    rw [← measure_univ_ne_zero, ← Metric.iUnion_ball_nat x, ne_eq,      measure_iUnion_null_iff, not_forall] at hμ    obtain ⟨n, hn⟩ := hμ    exact ⟨n, hn⟩  have hr' : 0 < r' := by    by_contra! hr'    simp [hr', Metric.ball_eq_empty.mpr] at h  refine h (nonpos_iff_eq_zero.mp ?_)  calc    μ (ball x r') ≤ As A (r' / r) * μ (ball x r) := by -- error if not in tactic mode        exact measure_ball_le_same x (by positivity) (div_mul_cancel₀ _ hr.ne').ge      _ = 0 := by rw [measure_mono_null hx h3U, mul_zero]