depth_lt_iff_not_disjoint

lemma depth_lt_iff_not_disjoint {d : ℝ} :    depth O x < ENNReal.ofReal d ↔ ¬Disjoint (ball x d) Oᶜ where  mp hd := by    simp_rw [depth, iSup_lt_iff, iSup_le_iff] at hd; obtain ⟨d', ld', hd'⟩ := hd    have ns := (hd' d.toNNReal).mt; rw [not_le] at ns; specialize ns ld'    rw [not_subset_iff_exists_mem_notMem] at ns; obtain ⟨y, my, ny⟩ := ns    have pd := zero_le.trans_lt ld'    rw [ofReal_pos] at pd; replace pd := Real.coe_toNNReal d pd.le    rw [pd] at my; exact not_disjoint_iff.mpr ⟨y, my, ny⟩  mpr hd := by    obtain ⟨y, my₁, my₂⟩ := not_disjoint_iff.mp hd    simp_rw [depth, iSup_lt_iff, iSup_le_iff]; use edist x y    rw [mem_ball'] at my₁; simp_rw [edist_lt_ofReal, my₁, true_and]; intro d' sd; by_contra! h    rw [← ofReal_coe_nnreal, edist_lt_ofReal, ← mem_ball'] at h    exact my₂ (sd h)