MeasureTheory.approx_above_superset

lemma approx_above_superset (t₀ : ℝ≥0∞) :    ⋃ n, (fun n : ℕ ↦ {x | t₀ + (↑n)⁻¹ < ‖f x‖ₑ}) n = {x | t₀ < ‖f x‖ₑ} := by  ext y  constructor <;> intro h  · obtain ⟨n, wn⟩ := exists_exists_eq_and.mp h    calc      t₀ ≤ t₀ + (↑n)⁻¹ := le_self_add      _  < ‖f y‖ₑ      := wn  · have h₁ : Iio (‖f y‖ₑ - t₀) ∈ 𝓝 0 := Iio_mem_nhds (tsub_pos_of_lt h)    have h₂ := ENNReal.tendsto_inv_nat_nhds_zero h₁    simp only [mem_map, mem_atTop_sets, mem_preimage, mem_Iio] at h₂    rcases h₂ with ⟨n, wn⟩    simpa using ⟨n, lt_tsub_iff_left.mp (wn n (Nat.le_refl n))⟩