Theorem: IntegrableAtFilter.sup_iff (PrimeNumberTheoremAnd/Mathlib/MeasureTheory/Integral/IntegrableOn.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup β
l✝ l'✝ : Filter α
f g : α → β
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f (l ⊔ l') μ ↔ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ
Tactic:
use fun h => ⟨h.filter_mono le_sup_left, h.filter_mono le_sup_right⟩
State after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup β
l✝ l'✝ : Filter α
f g : α → β
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ

State before:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup β
l✝ l'✝ : Filter α
f g : α → β
μ : Measure α
l l' : Filter α
⊢ IntegrableAtFilter f l μ ∧ IntegrableAtFilter f l' μ → IntegrableAtFilter f (l ⊔ l') μ
Tactic:
exact fun ⟨⟨s, hsl, hs⟩, ⟨t, htl, ht⟩⟩ ↦ ⟨s ∪ t, union_mem_sup hsl htl, hs.union ht⟩
State after:
no goals