MeasureTheory.IsDoubling.allBallsCoverBalls

lemma IsDoubling.allBallsCoverBalls [OpensMeasurableSpace X] [NeZero μ]    [IsLocallyFiniteMeasure μ] : AllBallsCoverBalls X 2 ⌈As A 9⌉₊ := by  classical  have := isOpenPosMeasure_of_isDoubling μ  have hA : A ≠ 0 := by    rintro rfl    exact NeZero.ne μ <| eq_zero_of_isDoubling_zero μ  refine .mk (by norm_num) fun r hr x ↦ ?_  set R := 2 * r  set R' := R + r / 2  set N : ℕ := ⌈As A 9⌉₊  let S := { s : Finset X | ↑s ⊆ ball x R ∧ ∀ x y, x ∈ s → y ∈ s → x ≠ y → r ≤ dist x y }  have h1 : ∀ s ∈ S, s.card ≤ N := by    by_contra!    obtain ⟨s, ⟨h1s, h2s⟩, h3s⟩ := this    let B := ⋃ y ∈ s, ball y (r / 2)    have : ∀ y ∈ s, (As A 9 : ℝ≥0∞)⁻¹ * μ (ball x R') ≤ μ (ball y (r / 2)) := by      intro y hy      rw [ENNReal.inv_mul_le_iff]      · apply measure_ball_le_of_dist_le' (by norm_num)        calc          dist y x + R' ≤ R + R' := by            gcongr            apply le_of_lt            simpa using h1s hy          _ ≤ 9 * (r / 2) := by simp_rw [R', R]; linarith      · simp [As, hA]      · simp    have lem : (s : Set X).PairwiseDisjoint fun y ↦ ball y (r / 2) := by      intro i hi j hj hij      refine Set.disjoint_left.mpr fun z hzi hzj ↦ ?_      exact lt_irrefl _ <| by calc        r ≤ dist i j := h2s i j hi hj hij        _ ≤ dist i z + dist z j := dist_triangle ..        _ < r / 2 + r / 2 := by gcongr; exacts [mem_ball'.mp hzi, mem_ball.mp hzj]        _ = r := by linarith    exact lt_irrefl _ <| calc      μ (ball x R') ≤ N * (As A 9 : ℝ≥0∞)⁻¹ * μ (ball x R') := by          conv_lhs => rw [← one_mul (μ _)]          gcongr          rw [← div_eq_mul_inv, ENNReal.le_div_iff_mul_le, one_mul]          · simp [N, Nat.le_ceil]          · simp [As, hA]          · simp      _ < s.card * (As A 9 : ℝ≥0∞)⁻¹ * μ (ball x R') := by          gcongr          · refine isOpen_ball.measure_ne_zero μ ?_            have : 0 < R' := by positivity            simp [this]          · exact IsDoubling.measure_ball_lt_top.ne          · simp [As]          · simp [As, hA]      _ = ∑ y ∈ s, (As A 9 : ℝ≥0∞)⁻¹ * μ (ball x R') := by          simp_rw [Finset.sum_const, nsmul_eq_mul, mul_assoc]      _ ≤ ∑ y ∈ s, μ (ball y (r / 2)) := by gcongr with i hi; exact this i hi      _ = μ (⋃ y ∈ s, ball y (r / 2)) := by          rw [measure_biUnion_finset lem]          intros; apply measurableSet_ball      _ ≤ μ (ball x R') := by          apply measure_mono          simp_rw [Set.iUnion_subset_iff]          intro i hi z hz          rw [mem_ball]          calc            dist z x ≤ dist z i + dist i x := dist_triangle ..            _ < r / 2 + R := by simp at hz; gcongr; simpa using h1s hi            _ = R' := by ring  have h1' : BddAbove ((·.card) '' S) := by    simp only [bddAbove_def, Set.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]    use N, h1  have h2 : S.Nonempty := ⟨∅, by simp, by simp⟩  obtain ⟨s, hs, s_max⟩ := Nat.exists_max_image h2 h1'  have := hs; obtain ⟨h1s, h2s⟩ := this  use s, h1 s hs  intro y hy  push _ ∈ _  simp only [mem_ball]  by_contra! h2y  have hys : y ∉ s := by intro h3y; simpa [hr.not_ge] using h2y y h3y  have h2 : insert y s ∈ S := by    suffices ∀ (x y_1 : X), x = y ∨ x ∈ s → y_1 = y ∨ y_1 ∈ s → ¬x = y_1 → r ≤ dist x y_1 by      simp [Set.subset_def, -Metric.mem_ball] at h1s      simp [S] at hs hy      simp [S, Set.insert_subset_iff, hs, hy, eq_true_intro this]    rintro u v (rfl|hu) (rfl|hv) huv    · simp at huv    · exact h2y v hv    · rw [dist_comm]; exact h2y u hu    · exact h2s u v hu hv huv  specialize s_max (insert y s) h2  simp [hys] at s_max