no goals
α : Type u_1
β : Type u_2
γ : Type ?u.691697
δ : Type ?u.691700
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
⊢ (∫⁻ (x : α), ↑‖0‖₊ ∂μ) = 0
simp