ENNReal.ofReal_Ioo_eq

lemma ENNReal.ofReal_Ioo_eq {a b : ℝ≥0∞} : ENNReal.ofReal ⁻¹' Set.Ioo a b    = if a = ⊤ then ∅ else if a ≤ b ∧ b = ∞ then Set.Ioi a.toReal else Set.Ioo a.toReal b.toReal := by  split_ifs with ha h  · rw [ha]    simp  · rw [h.2]    ext x    simp only [mem_preimage, mem_Ioo, ofReal_lt_top, and_true, mem_Ioi]    exact lt_ofReal_iff_toReal_lt ha  · ext x    simp only [mem_preimage, mem_Ioo]    push Not at h    by_cases hx : x < 0    · rw [ENNReal.ofReal_of_nonpos hx.le]      simp only [_root_.not_lt_zero, false_and, false_iff, not_and, not_lt]      intro ha      exfalso      have := ha.trans hx      have := @toReal_nonneg a      linarith    push Not at hx    constructor    · intro h'      rw [← ofReal_lt_iff_lt_toReal hx (by aesop)]      use toReal_lt_of_lt_ofReal h'.1, h'.2    · intro h'      rwa [lt_ofReal_iff_toReal_lt ha, ofReal_lt_iff_lt_toReal hx]      aesop