depth_bound_3

lemma depth_bound_3 (hO : O ≠ univ) (h : x ∈ ball y (3 * ((depth O y).toReal / 6))) :    (depth O y).toReal / 6 + dist y x ≤ 8 * (depth O x).toReal / 6 := by  rw [mem_ball'] at h  have dnt {z : X} : depth O z ≠ ⊤ := (depth_lt_top_iff_ne_univ.mpr hO).ne  have dnt2 : depth O y / 2 ≠ ⊤ := ENNReal.div_ne_top dnt (by norm_num)  have hti : depth O y ≤ 2 * depth O x := by    rw [mul_comm, ← ENNReal.div_le_iff_le_mul (.inl (by norm_num)) (.inl (by norm_num)),      ← ENNReal.add_le_add_iff_left dnt2, ENNReal.add_halves]    calc      _ ≤ edist y x + depth O x := depth_le_edist_add_depth      _ ≤ _ := by        gcongr; rw [edist_dist]; apply ofReal_le_of_le_toReal        rw [toReal_div, toReal_ofNat]; linarith  calc    _ ≤ (2 * depth O x).toReal / 6 + 3 * ((depth O y).toReal / 6) := by gcongr; have := @dnt x; finiteness    _ ≤ (2 * depth O x).toReal / 6 + 3 * ((2 * depth O x).toReal / 6) := by gcongr; have := @dnt x; finiteness    _ = _ := by rw [toReal_mul, toReal_ofNat]; ring