-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem Measure.FiniteAtFilter.integrableAtFilter {l : Filter α} [IsMeasurablyGenerated l]
    (hfm : StronglyMeasurableAtFilter f l μ) (hμ : μ.FiniteAtFilter l)
    (hf : l.IsBoundedUnder (· ≤ ·) (norm ∘ f)) : IntegrableAtFilter f l μ

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
⊢ IntegrableAtFilter f l μ

Tactic:
obtain ⟨C, hC⟩ : ∃ C, ∀ᶠ s in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C :=
  hf.imp fun C hC => eventually_smallSets.2 ⟨_, hC, fun t => id⟩

Result:
case intro
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l μ

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ✝ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : μ s < ⊤
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l μ

Tactic:
refine ⟨s, hsl, ⟨hfm, hasFiniteIntegral_restrict_of_bounded hμ (C := C) ?_⟩⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ✝ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : μ s < ⊤
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ✝ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : μ s < ⊤
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C

Tactic:
exact Eventually.of_forall hC

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ✝ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : μ s < ⊤
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C

Tactic:
rw [ae_restrict_eq hsm, eventually_inf_principal]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ✝ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : μ s < ⊤
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C

Proof state:
case intro
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l μ

Tactic:
rcases (hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_smallSets with
  ⟨s, hsl, hsm, hfm, hμ, hC⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
inst✝ : l.IsMeasurablyGenerated
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ✝ : μ.FiniteAtFilter l
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f)
C : ℝ
hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfm : AEStronglyMeasurable f (μ.restrict s)
hμ : μ s < ⊤
hC : ∀ x ∈ s, ‖f x‖ ≤ C
⊢ IntegrableAtFilter f l μ