Vitali covering lemma

theorem vitali_covering_lemma    {ι : Type*} {x : ι → E} {r : ι → ℝ}    (hr_pos : ∀ i, 0 < r i)    (hr_bdd : BddAbove (Set.range r))    (hfin : (⋃ i, Metric.ball (x i) (r i)).Nonempty) :    ∃ S : Set ι, S.Countable ∧      (∀ i ∈ S, ∀ j ∈ S, i ≠ j →        Disjoint (Metric.ball (x i) (r i)) (Metric.ball (x j) (r j))) ∧      (∀ i, ∃ j ∈ S,        (Metric.ball (x i) (r i) ∩ Metric.ball (x j) (r j)).Nonempty ∧ r i ≤ 2 * r j) ∧      (⋃ i, Metric.ball (x i) (r i)) ⊆ ⋃ i ∈ S, Metric.ball (x i) (5 * r i) := by  classical  let _ := hfin  let t : Set ι := Set.univ  obtain ⟨R, hR⟩ := hr_bdd  rcases      Vitali.exists_disjoint_subfamily_covering_enlargement        (fun i => Metric.ball (x i) (r i)) t r 2 (by norm_num)        (fun i _ => (hr_pos i).le) R (by          intro i hi          exact hR (Set.mem_range_self i)) (fun i _ =>            nonempty_ball.2 (hr_pos i))    with ⟨S, _, hS_disj, hS_hit⟩  have hS_ball_disj : S.PairwiseDisjoint (fun i => Metric.ball (x i) (r i)) := by    exact hS_disj  have hS_count : S.Countable := by    exact hS_ball_disj.countable_of_isOpen      (fun i _ => isOpen_ball)      (fun i _ => nonempty_ball.2 (hr_pos i))  refine ⟨S, hS_count, ?_, ?_, ?_⟩  · intro i hi j hj hij    exact hS_ball_disj hi hj hij  · intro i    rcases hS_hit i (by simp [t]) with ⟨j, hjS, hij, hrad⟩    exact ⟨j, hjS, hij, hrad⟩  · intro y hy    rcases Set.mem_iUnion.1 hy with ⟨i, hyi⟩    rcases hS_hit i (by simp [t]) with ⟨j, hjS, hij, hrad⟩    refine Set.mem_iUnion.2 ⟨j, Set.mem_iUnion.2 ⟨hjS, ?_⟩⟩    rcases hij with ⟨z, hzi, hzj⟩    have hyj : dist y (x j) < 5 * r j := by      calc        dist y (x j) ≤ dist y (x i) + dist (x i) z + dist z (x j) :=          dist_triangle4 y (x i) z (x j)        _ < r i + r i + r j := by          have h1 : dist y (x i) < r i := by simpa [Metric.mem_ball] using hyi          have h2 : dist (x i) z < r i := by rw [dist_comm]; simpa [Metric.mem_ball] using hzi          have h3 : dist z (x j) < r j := by simpa [Metric.mem_ball] using hzj          linarith        _ ≤ 5 * r j := by linarith    exact hyj