ae_volume_of_contains_compl_singleton_zero

theorem ae_volume_of_contains_compl_singleton_zero  (s : Set ℝ)  (h : (univ : Set ℝ) \ {0} ⊆ s) :  s ∈ (MeasureTheory.ae volume) := by  -- The key insight is that {0} has measure zero in ℝ  have h_zero_null : volume ({0} : Set ℝ) = 0 := by    exact volume_singleton   -- Since s contains univ \ {0} = ℝ \ {0}, its complement is contained in {0}  have h_compl_subset : sᶜ ⊆ {0} := by    intro x hx    -- If x is not in s, then x is not in ℝ \ {0} (since ℝ \ {0} is a subset of s)    -- This means x = 0    by_contra h_not_zero    have : x ∈ univ \ {0} := ⟨trivial, h_not_zero⟩    exact hx (h this)   -- Therefore, volume(sᶜ) ≤ volume({0}) = 0  have h_compl_measure : volume sᶜ ≤ volume ({0} : Set ℝ) :=    measure_mono h_compl_subset   -- So volume(sᶜ) = 0  have h_compl_zero : volume sᶜ = 0 := by    rw [h_zero_null] at h_compl_measure    exact le_antisymm h_compl_measure (by positivity)   -- A set is in ae.sets iff its complement has measure zero  rwa [mem_ae_iff]