depth_lt_top_iff_ne_univ

lemma depth_lt_top_iff_ne_univ : depth O x < ⊤ ↔ O ≠ univ := by  constructor <;> intro h  · contrapose! h; simp_rw [top_le_iff, depth, iSup₂_eq_top, h, subset_univ, exists_const]    intro r rlt; lift r to ℝ≥0 using rlt.ne    use r + 1; exact coe_lt_coe_of_lt (lt_add_one r)  · obtain ⟨p, np⟩ := (ne_univ_iff_exists_notMem _).mp h    calc      _ ≤ edist x p := by        refine iSup₂_le fun r hr ↦ ?_        contrapose! hr; rw [not_subset]; use p, ?_, np        rw [coe_nnreal_eq, edist_dist, ofReal_lt_ofReal_iff_of_nonneg dist_nonneg] at hr        rwa [mem_ball']      _ < _ := edist_lt_top ..