no goals
α : Type u_1
β : Type u_2
γ : Type ?u.721423
δ : Type ?u.721426
m✝ : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
m : MeasurableSpace α
f : α → β
⊢ HasFiniteIntegral f
simp only [HasFiniteIntegral, lintegral_zero_measure, WithTop.zero_lt_top]