awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal (max 1 (I + 1))

Tactic:
htendsto.eventually (ge_mem_nhds ?_)

Premises used: ge_mem_nhds, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
refine : ENNReal.ofReal I < ENNReal.ofReal (max 1 (I + 1))
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal (max 1 (I + 1))

Tactic:
refine htendsto.eventually (ge_mem_nhds ?_)

Premises used: ge_mem_nhds, Filter.Tendsto.eventually
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ ENNReal.ofReal I < ENNReal.ofReal (max 1 (I + 1))

Tactic:
(ENNReal.ofReal_lt_ofReal_iff (lt_max_of_lt_left zero_lt_one)).2 ?_

Premises used: Iff.mpr, lt_max_of_lt_left, zero_lt_one, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
refine : I < max 1 (I + 1)
⊢ ENNReal.ofReal I < ENNReal.ofReal (max 1 (I + 1))

Tactic:
refine (ENNReal.ofReal_lt_ofReal_iff (lt_max_of_lt_left zero_lt_one)).2 ?_

Premises used: Iff.mpr, lt_max_of_lt_left, zero_lt_one, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ I < max 1 (I + 1)

Tactic:
lt_max_of_lt_right (lt_add_one I)

Premises used: lt_add_one, lt_max_of_lt_right
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal I))
⊢ I < max 1 (I + 1)

Tactic:
exact lt_max_of_lt_right (lt_add_one I)

Premises used: lt_add_one, lt_max_of_lt_right
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ≥0
hfm : AEStronglyMeasurable f μ
hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ (↑I : ℝ≥0∞)
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal (↑I : ℝ)

Tactic:
simpa only [ENNReal.ofReal_coe_nnreal] using hbounded

Premises used: ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ≥0
hfm : AEStronglyMeasurable f μ
htendsto : Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (↑I : ℝ≥0∞))
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ) l (𝓝 (ENNReal.ofReal (↑I : ℝ)))

Tactic:
simpa only [ENNReal.ofReal_coe_nnreal] using htendsto

Premises used: ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
⊢ AEStronglyMeasurable f μ

Tactic:
have hfm : AEStronglyMeasurable f μ :=
    hφ.aestronglyMeasurable fun i => (hfi i).aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
⊢ Integrable f μ

Tactic:
hφ.integrable_of_lintegral_enorm_bounded I hfm ?_

Premises used: MeasureTheory.AECover.integrable_of_lintegral_enorm_bounded
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
refine : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
⊢ Integrable f μ

Tactic:
refine hφ.integrable_of_lintegral_enorm_bounded I hfm ?_

Premises used: MeasureTheory.AECover.integrable_of_lintegral_enorm_bounded
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
rw : (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal
| ∫ (x : α) in φ i, ‖f x‖ ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x))
        hfm.norm.restrict]

Premises used: MeasureTheory.AEStronglyMeasurable.restrict, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.ae_of_all, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I

Tactic:
conv at hbounded in integral _ _ =>
    rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x))
        hfm.norm.restrict]

Premises used: MeasureTheory.AEStronglyMeasurable.restrict, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.ae_of_all, MeasureTheory.integral, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I
hfm : AEStronglyMeasurable f μ
hbounded₁ : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
⊢ AEStronglyMeasurable f μ

Tactic:
conv at hbounded in integral _ _ =>
    rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x))
        hfm.norm.restrict]

Premises used: MeasureTheory.AEStronglyMeasurable.restrict, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.ae_of_all, MeasureTheory.integral, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
a : α
rw : (↑‖f a‖₊ : ℝ≥0∞)
| ENNReal.ofReal ‖f a‖

Tactic:
rw [← coe_nnnorm, ENNReal.ofReal_coe_nnreal]

Premises used: coe_nnnorm, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I

Tactic:
conv at hbounded in ENNReal.ofReal _ =>
    rw [← coe_nnnorm, ENNReal.ofReal_coe_nnreal]

Premises used: ENNReal.ofReal, coe_nnnorm, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
hbounded₁ : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
⊢ AEStronglyMeasurable f μ

Tactic:
conv at hbounded in ENNReal.ofReal _ =>
    rw [← coe_nnnorm, ENNReal.ofReal_coe_nnreal]

Premises used: ENNReal.ofReal, coe_nnnorm, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I

Tactic:
hbounded.mono fun i hi => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
refine :
  ∀ (i : ι) (hi : (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I), ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I
⊢ ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I

Tactic:
refine hbounded.mono fun i hi => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
hi : (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
rw : ENNReal.ofReal (∫⁻ (a : α) in φ i, ‖f a‖ₑ ∂μ).toReal ≤ ENNReal.ofReal I
⊢ ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I

Tactic:
rw [← ENNReal.ofReal_toReal <| ne_top_of_lt <| hasFiniteIntegral_iff_enorm.mp (hfi i).2]

Premises used: ENNReal.ofReal_toReal, And.right, Iff.mp, ne_top_of_lt, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
hfm : AEStronglyMeasurable f μ
i : ι
hi : (∫⁻ (a : α) in φ i, (↑‖f a‖₊ : ℝ≥0∞) ∂μ).toReal ≤ I
⊢ ENNReal.ofReal (∫⁻ (a : α) in φ i, ‖f a‖ₑ ∂μ).toReal ≤ ENNReal.ofReal I

Tactic:
apply ENNReal.ofReal_le_ofReal hi

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : l.NeBot
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
htendsto : Tendsto (fun (i : ι) ↦ ∫ (x : α) in φ i, ‖f x‖ ∂μ) l (𝓝 I)
⊢ Integrable f μ

Tactic:
let ⟨I', hI'⟩ := htendsto.isBoundedUnder_le
  hφ.integrable_of_integral_norm_bounded I' hfi hI'

Premises used: Filter.Tendsto.isBoundedUnder_le, MeasureTheory.AECover.integrable_of_integral_norm_bounded, MeasureTheory.Integrable, _private.0.MeasureTheory.AECover.integrable_of_integral_norm_tendsto.match_1
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : l.NeBot
inst_2 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hnng : ∀ᵐ (x : α) ∂μ, 0 ≤ f x
hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, f x ∂μ ≤ I
⊢ Integrable f μ

Tactic:
hφ.integrable_of_integral_norm_bounded I hfi <| hbounded.mono fun _i hi =>
    (integral_congr_ae <| ae_restrict_of_ae <| hnng.mono fun _ => Real.norm_of_nonneg).le.trans hi

Premises used: MeasureTheory.AECover.integrable_of_integral_norm_bounded, MeasureTheory.integral_congr_ae, Eq.le, MeasureTheory.ae_restrict_of_ae, Filter.Eventually.mono, LE.le.trans, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : l.NeBot
inst_2 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (φ i) μ
hnng : ∀ᵐ (x : α) ∂μ, 0 ≤ f x
htendsto : Tendsto (fun (i : ι) ↦ ∫ (x : α) in φ i, f x ∂μ) l (𝓝 I)
⊢ Integrable f μ

Tactic:
let ⟨I', hI'⟩ := htendsto.isBoundedUnder_le
  hφ.integrable_of_integral_bounded_of_nonneg_ae I' hfi hnng hI'

Premises used: Filter.Tendsto.isBoundedUnder_le, MeasureTheory.Integrable, _private.0.MeasureTheory.AECover.integrable_of_integral_tendsto_of_nonneg_ae.match_1, MeasureTheory.AECover.integrable_of_integral_bounded_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto.{u_2, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
⊢ Tendsto.{u_2, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
h
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto.{u_2, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
h₁ : ∀ (x : ι), Eq.{u_3 + 1} (α := E) (∫ (x : α) in φ x, f x ∂μ) (∫ (x_1 : α), (φ x).indicator f x_1 ∂μ)
⊢ Tendsto.{u_2, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : α) in φ i, f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
convert! h using 2
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto.{u_2, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x : ι
h₁ h₂ : Eq.{u_3 + 1} (α := E) (∫ (x : α) in φ x, f x ∂μ) (∫ (x : α) in φ x, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in φ x, f x ∂μ) (∫ (x_1 : α), (φ x).indicator f x_1 ∂μ)

Tactic:
rw [integral_indicator (hφ.measurableSet _)]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.AECover.measurableSet
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
E : Type u_3
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : l.NeBot
inst_4 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
I : E
hfi : Integrable f μ
h : Tendsto (fun (n : ι) ↦ ∫ (x : α) in φ n, f x ∂μ) l (𝓝 I)
⊢ ∫ (x : α), f x ∂μ = I

Tactic:
tendsto_nhds_unique (hφ.integral_tendsto_of_countably_generated hfi) h

Premises used: MeasureTheory.AECover.integral_tendsto_of_countably_generated, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
α : Type u_1
ι : Type u_2
inst : MeasurableSpace α
μ : Measure α
l : Filter ι
inst_1 : l.NeBot
inst_2 : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → ℝ
I : ℝ
hnng : 0 ≤ᶠ[ae μ] f
hfi : ∀ (n : ι), IntegrableOn f (φ n) μ
htendsto : Tendsto (fun (n : ι) ↦ ∫ (x : α) in φ n, f x ∂μ) l (𝓝 I)
⊢ ∫ (x : α), f x ∂μ = I

Tactic:
have hfi' : Integrable f μ := hφ.integrable_of_integral_tendsto_of_nonneg_ae I hfi hnng htendsto
  hφ.integral_eq_of_tendsto I hfi' htendsto

Premises used: MeasureTheory.AECover.integral_eq_of_tendsto, MeasureTheory.AECover.integrable_of_integral_tendsto_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
⊢ AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)

Tactic:
have hφ : AECover μ l _ := aecover_Ioc ha hb
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)
⊢ Integrable f μ

Tactic:
hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)

Premises used: MeasureTheory.AECover.integrable_of_integral_norm_bounded, Filter.Eventually.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)
refine : ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ ≤ I
⊢ Integrable f μ

Tactic:
refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)

Premises used: MeasureTheory.AECover.integrable_of_integral_norm_bounded, Filter.Eventually.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)
h₁ :
  ∀ (i : ι) (hai : a i ≤ 0) (hbi : 0 ≤ b i) (ht : ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I),
    ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ ≤ I
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ ≤ I

Tactic:
filter_upwards [ha.eventually (eventually_le_atBot 0),
    hb.eventually (eventually_ge_atTop 0)] with i hai hbi ht

Premises used: Filter.Tendsto.eventually, Filter.eventually_ge_atTop, Filter.eventually_le_atBot, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
ht h₁ h₂ h₃ h₄ : ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ ≤ I

Tactic:
rwa [← intervalIntegral.integral_of_le (hai.trans hbi)]

Premises used: intervalIntegral.integral_of_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) l (𝓝 I)
⊢ Integrable f μ

Tactic:
let ⟨I', hI'⟩ := h.isBoundedUnder_le
  integrable_of_intervalIntegral_norm_bounded I' hfi ha hb hI'

Premises used: Filter.Tendsto.isBoundedUnder_le, MeasureTheory.Integrable, _private.0.MeasureTheory.integrable_of_intervalIntegral_norm_tendsto.match_1, MeasureTheory.integrable_of_intervalIntegral_norm_bounded
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a : ι → ℝ
f : ℝ → E
I b : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
⊢ AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)

Tactic:
have hφ : AECover (μ.restrict <| Iic b) l _ := aecover_Ioi ha