use fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderBot X
inst✝ : CompactIccSpace X
⊢ Integrable f μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ
case mpr
X : Type u_1
E : Type u_2
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝² : LinearOrder X
inst✝¹ : OrderBot X
inst✝ : CompactIccSpace X
⊢ IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ → Integrable f μ