Theorem: integrable_iff_integrableAtFilter_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✝¹ : OrderBot X
inst✝ : CompactIccSpace X
⊢ Integrable f μ ↔ IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ
Tactic:
use fun hf ↦ ⟨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✝¹ : OrderBot X
inst✝ : CompactIccSpace X
⊢ 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✝¹ : OrderBot X
inst✝ : CompactIccSpace X
⊢ 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✝¹ : OrderBot X
inst✝ : CompactIccSpace X
h : 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✝¹ : OrderBot X
inst✝ : CompactIccSpace X
h : IntegrableAtFilter f atTop μ ∧ LocallyIntegrable f μ
⊢ IntegrableAtFilter f (cocompact X) μ
Tactic:
exact h.1.filter_mono cocompact_le_atTop
State after:
no goals