rw [ENNReal.toNNReal_eq_zero_iff] at hz
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = 0
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False
case mk.inl
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ↑↑q s = 0 ∨ ↑↑q s = ⊤
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
hz_zero : z = 0
⊢ False