depth_bound_2

lemma depth_bound_2 (hO : O ≠ univ) (h : x ∈ ball y (3 * ((depth O y).toReal / 6))) :    (depth O x).toReal / 6 + dist x y ≤ 8 * (depth O y).toReal / 6 := by  rw [mem_ball] at h  have ent : edist x y ≠ ⊤ := by finiteness  have dnt {z : X} : depth O z ≠ ⊤ := (depth_lt_top_iff_ne_univ.mpr hO).ne  calc    _ ≤ (edist x y + depth O y).toReal / 6 + dist x y := by      gcongr      · rw [ENNReal.add_ne_top]; exact ⟨ent, dnt⟩      · exact depth_le_edist_add_depth    _ = (depth O y).toReal / 6 + (7 / 6) * dist x y := by      rw [ENNReal.toReal_add ent dnt, ← dist_edist]; ring    _ ≤ (depth O y).toReal / 6 + (7 / 6) * (3 * ((depth O y).toReal / 6)) := by gcongr    _ = (9 / 2) * (depth O y).toReal / 6 := by ring    _ ≤ _ := by gcongr; norm_num