ENNReal set averages in Mathlib: x/0 = ∞ and ∞/∞ = 0 traps
setLAverage_eq rewrites ⨍⁻ x in s, f x ∂μ to (∫⁻ x in s, f x ∂μ) / μ s. In ℝ≥0∞, c / 0 = ∞ for c ≠ 0, so after rewriting, 'μ s = 0 ⇒ average = 0' is not automatic: you must also rewrite the integral to 0 with setLIntegral_measure_zero _ _ hμs. Likewise a bound of the form C * I / t with I = ∞ is NOT ∞ when t = ∞ (∞/∞ = ∞ * 0 = 0), so case-split t = ∞ separately (usually the superlevel set {∞ < F} is empty by not_top_lt). Useful conversions: from t < I / μs get t * μs ≤ I via (ENNReal.le_div_iff_mul_le (Or.inr hI0) (Or.inr hIfin)).1 h.le; and (t * μ s) / μ s ≤ t by ENNReal.div_le_of_le_mul le_rfl.
Checked on Mathlib v4.35.0. (∞ : ℝ≥0∞) / ∞ = 0 closes by simp, and c / 0 = ∞ for c ≠ 0 is ENNReal.div_zero h. simp [h] does not do the latter by itself ('simp made no progress'), so cite the lemma. setLAverage_eq, setLIntegral_measure_zero (μ s = 0 → ∫⁻ x in s, f x ∂μ = 0), ENNReal.le_div_iff_mul_le (b ≠ 0 ∨ c ≠ 0 → b ≠ ∞ ∨ c ≠ ∞ → (a ≤ c / b ↔ a * b ≤ c)), ENNReal.div_le_of_le_mul and not_top_lt all have the shapes used here. setLAverage_eq and setLIntegral_measure_zero are in MeasureTheory, so open it.