Metric.eannulusIoc_ofReal

lemma eannulusIoc_ofReal (hr : 0 ≤ r) :    eannulusIoc x (ENNReal.ofReal r) (ENNReal.ofReal R) = annulusIoc x r R := by  ext y  constructor  · intro hy    have hy' :        ENNReal.ofReal r < ENNReal.ofReal (dist y x) ∧          ENNReal.ofReal (dist y x) ≤ ENNReal.ofReal R := by      simpa [eannulusIoc, edist_dist, annulusIoc, mem_Ioc] using hy    have hrd : r < dist y x :=      (ENNReal.ofReal_lt_ofReal_iff_of_nonneg hr).1 hy'.1    have hpos : ¬dist y x ≤ 0 := not_le_of_gt (lt_of_le_of_lt hr hrd)    have hle : dist y x ≤ R := by      have hle' : dist y x ≤ R ∨ dist y x ≤ 0 :=        (ENNReal.ofReal_le_ofReal_iff').1 hy'.2      exact hle'.resolve_right hpos    simp [annulusIoc, mem_Ioc, hrd, hle]  · intro hy    have hy' : r < dist y x ∧ dist y x ≤ R := by      simpa [annulusIoc, mem_Ioc] using hy    have : ENNReal.ofReal r < ENNReal.ofReal (dist y x) :=      (ENNReal.ofReal_lt_ofReal_iff_of_nonneg hr).2 hy'.1    have : (ENNReal.ofReal r < ENNReal.ofReal (dist y x)) ∧        (ENNReal.ofReal (dist y x) ≤ ENNReal.ofReal R) :=      ⟨this, ENNReal.ofReal_le_ofReal hy'.2⟩    simpa [eannulusIoc, edist_dist, annulusIoc, mem_Ioc] using this