depth_bound_1

lemma depth_bound_1 (hO : O ≠ univ)    (h : ¬Disjoint (ball x ((depth O x).toReal / 6)) (ball y ((depth O y).toReal / 6))) :    x ∈ ball y (3 * ((depth O y).toReal / 6)) := by  rw [mem_ball]  have dnt {z : X} : depth O z ≠ ⊤ := (depth_lt_top_iff_ne_univ.mpr hO).ne  have pre : depth O x / 6 + 5 * depth O x / 6 ≤ depth O x / 6 + 7 * depth O y / 6 := by    calc      _ = depth O x := by        rw [← ENNReal.add_div, ← one_add_mul, show (1 : ℝ≥0∞) + 5 = 6 by norm_num, mul_comm]        exact ENNReal.mul_div_cancel_right (by norm_num) (by norm_num)      _ ≤ edist x y + depth O y := depth_le_edist_add_depth      _ ≤ ENNReal.ofReal ((depth O x).toReal / 6 + (depth O y).toReal / 6) + depth O y := by        rw [edist_dist]        exact add_le_add_left (ofReal_le_ofReal (dist_lt_of_not_disjoint_ball h).le) _      _ ≤ depth O x / 6 + depth O y / 6 + depth O y := by        rw [ofReal_add (by positivity) (by positivity)]        iterate 2 rw [ofReal_div_of_pos (by norm_num), ofReal_ofNat, ofReal_toReal dnt]      _ = _ := by        rw [show (7 : ℝ≥0∞) = 1 + 6 by norm_num, one_add_mul, ENNReal.add_div, mul_comm,          ENNReal.mul_div_cancel_right (by norm_num) (by norm_num), add_assoc]  rw [ENNReal.add_le_add_iff_left (div_ne_top dnt (by norm_num)),    ENNReal.div_le_iff (by norm_num) (by norm_num),    ENNReal.div_mul_cancel (by norm_num) (by norm_num), mul_comm,    ← ENNReal.le_div_iff_mul_le (.inl (by norm_num)) (.inl (by norm_num)),    ENNReal.mul_div_right_comm] at pre  calc    _ < (depth O x).toReal / 6 + (depth O y).toReal / 6 := dist_lt_of_not_disjoint_ball h    _ ≤ (7 / 5 * depth O y).toReal / 6 + (depth O y).toReal / 6 := by      gcongr; exact mul_ne_top (by finiteness) dnt    _ ≤ 2 * (depth O y).toReal / 6 + (depth O y).toReal / 6 := by      nth_rw 3 [← toReal_ofNat]; rw [← toReal_mul]; gcongr      · exact mul_ne_top (by finiteness) dnt      · rw [ENNReal.div_le_iff_le_mul (.inl (by norm_num)) (.inl (by norm_num))]        norm_num    _ = _ := by rw [mul_div_assoc, ← add_one_mul, two_add_one_eq_three]