rw [ENNReal.coe_toNNReal hq_fin.ne]
case hz'
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) = z
hq_fin : ↑↑q s < ⊤
⊢ ↑↑q s = ↑(ENNReal.toNNReal (↑↑q s))
no goals