no goals
α : Type u_1
β : Type u_2
γ : Type ?u.854853
δ : Type ?u.854856
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
inst✝ : IsFiniteMeasure μ
f : α → β
h : μ = 0
⊢ Integrable f ↔ Integrable f
simp [h]