Theorem: integrable_iff_integrableAtFilter_atBot_atTop (PrimeNumberTheoremAnd/Mathlib/MeasureTheory/Function/LocallyIntegrable.lean)

State before:
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✝ : CompactIccSpace X
⊢ Integrable f μ ↔ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
Tactic:
use fun hf ↦ ⟨⟨hf.integrableAtFilter _, hf.integrableAtFilter _⟩, hf.locallyIntegrable⟩
State after:
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✝ : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ

State before:
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✝ : CompactIccSpace X
⊢ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ → Integrable f μ
Tactic:
refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
State after:
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✝ : CompactIccSpace X
h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ

State before:
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✝ : CompactIccSpace X
h : (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
Tactic:
exact (IntegrableAtFilter.sup_iff.mpr h.1).filter_mono cocompact_le_atBot_atTop
State after:
no goals