awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
i : ι
rw : Integrable f (μ.restrict (Ioi (a i) ∩ Iic b))
⊢ IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))

Tactic:
rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i)]

Premises used: MeasureTheory.AECover.measurableSet, MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_restrict
-- 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
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
i : ι
⊢ Integrable f (μ.restrict (Ioi (a i) ∩ Iic b))

Tactic:
hfi i

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, MeasureTheory.IntegrableOn, Set.inter, Set.Iic
-- 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
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
i : ι
⊢ Integrable f (μ.restrict (Ioi (a i) ∩ Iic b))

Tactic:
exact hfi i
-- 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
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
⊢ ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))

Tactic:
have hfi : ∀ i, IntegrableOn f (Ioi (a i)) (μ.restrict <| Iic b) := by
    intro i
    rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i)]
    exact hfi i
-- 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_1 : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
⊢ IntegrableOn f (Iic b) μ

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

Premises used: MeasureTheory.AECover.integrable_of_integral_norm_bounded, MeasureTheory.IntegrableOn, 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 : ι → ℝ
f : ℝ → E
I b : ℝ
hfi_1 : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
refine : ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a x), ‖f x‖ ∂μ.restrict (Iic b) ≤ I
⊢ IntegrableOn f (Iic b) μ

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 : ι → ℝ
f : ℝ → E
I b : ℝ
hfi_1 : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
h₁ :
  ∀ (i : ι) (hai : a i ≤ b), ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i), ‖f x‖ ∂μ.restrict (Iic b) ≤ I
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a x), ‖f x‖ ∂μ.restrict (Iic b) ≤ I

Tactic:
filter_upwards [ha.eventually (eventually_le_atBot b)] with i hai

Premises used: Filter.Tendsto.eventually, Filter.eventually_le_atBot
-- 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_1 : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
i : ι
hai : a i ≤ b
h₁ : ∫ (x : ℝ) in Ioc (a i) b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i) ∩ Iic b, ‖f x‖ ∂μ ≤ I
⊢ ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i), ‖f x‖ ∂μ.restrict (Iic b) ≤ I

Tactic:
rw [intervalIntegral.integral_of_le hai, Measure.restrict_restrict (hφ.measurableSet i)]

Premises used: MeasureTheory.AECover.measurableSet, MeasureTheory.Measure.restrict_restrict, intervalIntegral.integral_of_le
-- 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_1 : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in Ioc (a i) b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i) ∩ Iic b, ‖f x‖ ∂μ ≤ I

Tactic:
id

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, id, Set.inter, Set.Iic
-- 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_1 : ∀ (i : ι), IntegrableOn f (Ioc (a i) b) μ
ha : Tendsto a l atBot
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
hfi : ∀ (i : ι), IntegrableOn f (Ioi (a i)) (μ.restrict (Iic b))
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in Ioc (a i) b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i) ∩ Iic b, ‖f x‖ ∂μ ≤ I

Tactic:
exact id

Premises used: id
-- 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 : Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ) l (𝓝 I)
⊢ IntegrableOn f (Iic b) μ

Tactic:
let ⟨I', hI'⟩ := h.isBoundedUnder_le
  integrableOn_Iic_of_intervalIntegral_norm_bounded I' b hfi ha hI'

Premises used: Filter.Tendsto.isBoundedUnder_le, MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_bounded, MeasureTheory.IntegrableOn, _private.0.MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto.match_1, Set.Iic
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
⊢ AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)

Tactic:
have hφ : AECover (μ.restrict <| Ioi a) l _ := aecover_Iic 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
i : ι
rw : Integrable f (μ.restrict (Ioi a ∩ Iic (b i)))
⊢ IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))

Tactic:
rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]

Premises used: MeasureTheory.AECover.measurableSet, MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_restrict, Set.inter_comm
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
i : ι
⊢ Integrable f (μ.restrict (Ioi a ∩ Iic (b i)))

Tactic:
hfi i

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, MeasureTheory.IntegrableOn, Set.inter, Set.Iic
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
i : ι
⊢ Integrable f (μ.restrict (Ioi a ∩ Iic (b i)))

Tactic:
exact hfi i
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
⊢ ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))

Tactic:
have hfi : ∀ i, IntegrableOn f (Iic (b i)) (μ.restrict <| Ioi a) := by
    intro i
    rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
    exact hfi i
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi_1 : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
⊢ IntegrableOn f (Ioi a) μ

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

Premises used: MeasureTheory.AECover.integrable_of_integral_norm_bounded, MeasureTheory.IntegrableOn, 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi_1 : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
refine : ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
⊢ IntegrableOn f (Ioi a) μ

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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi_1 : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
h₁ :
  ∀ (i : ι) (hbi : a ≤ b i), ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I

Tactic:
filter_upwards [hb.eventually (eventually_ge_atTop a)] with i hbi

Premises used: Filter.Tendsto.eventually, Filter.eventually_ge_atTop
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi_1 : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
i : ι
hbi : a ≤ b i
h₁ : ∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ ≤ I
⊢ ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I

Tactic:
rw [intervalIntegral.integral_of_le hbi, Measure.restrict_restrict (hφ.measurableSet i),
    inter_comm]

Premises used: MeasureTheory.AECover.measurableSet, MeasureTheory.Measure.restrict_restrict, intervalIntegral.integral_of_le, Set.inter_comm
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi_1 : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ ≤ I

Tactic:
id

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, id, Set.inter, Set.Iic
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi_1 : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
hfi : ∀ (i : ι), IntegrableOn f (Iic (b i)) (μ.restrict (Ioi a))
i : ι
hbi : a ≤ b i
⊢ ∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ ≤ I

Tactic:
exact id

Premises used: id
-- 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
b : ι → ℝ
f : ℝ → E
I a : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc a (b i)) μ
hb : Tendsto b l atTop
h : Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) l (𝓝 I)
⊢ IntegrableOn f (Ioi a) μ

Tactic:
let ⟨I', hI'⟩ := h.isBoundedUnder_le
  integrableOn_Ioi_of_intervalIntegral_norm_bounded I' a hfi hb hI'

Premises used: Filter.Tendsto.isBoundedUnder_le, Set.Ioi, MeasureTheory.IntegrableOn, MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_bounded, _private.0.MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto.match_1
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤
      I
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioc a₀ b₀) volume

Tactic:
(aecover_Ioc_of_Ioc ha hb).integrable_of_integral_norm_bounded I
    (fun i => (hfi i).restrict) (h.mono fun i hi ↦ ?_)

Premises used: MeasureTheory.AECover.integrable_of_integral_norm_bounded, MeasureTheory.IntegrableOn, Filter.Eventually.mono, MeasureTheory.aecover_Ioc_of_Ioc, MeasureTheory.IntegrableOn.restrict
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤
      I
refine :
  ∀ (i : ι)
    (hi :
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦
          ‖f x‖) ≤
        I),
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.restrict volume (Ioc a₀ b₀)) (Ioc (a i) (b i)))
        fun (x : ℝ) ↦ ‖f x‖) ≤
      I
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioc a₀ b₀) volume

Tactic:
refine (aecover_Ioc_of_Ioc ha hb).integrable_of_integral_norm_bounded I
    (fun i => (hfi i).restrict) (h.mono fun i hi ↦ ?_)

Premises used: MeasureTheory.AECover.integrable_of_integral_norm_bounded, Filter.Eventually.mono, MeasureTheory.aecover_Ioc_of_Ioc, MeasureTheory.IntegrableOn.restrict
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤
      I
i : ι
hi :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤ I
rw :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc (a i) (b i) ∩ Ioc a₀ b₀)) fun (x : ℝ) ↦ ‖f x‖) ≤
    I
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.restrict volume (Ioc a₀ b₀)) (Ioc (a i) (b i)))
      fun (x : ℝ) ↦ ‖f x‖) ≤
    I

Tactic:
rw [Measure.restrict_restrict measurableSet_Ioc]

Premises used: MeasureTheory.Measure.restrict_restrict, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤
      I
i : ι
hi :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤ I
grw :
  LE.le (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc (a i) (b i) ∩ Ioc a₀ b₀)) fun (x : ℝ) ↦ ‖f x‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖)
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc (a i) (b i) ∩ Ioc a₀ b₀)) fun (x : ℝ) ↦ ‖f x‖) ≤
    I

Tactic:
grw [← hi]
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤
      I
i : ι
hi :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤ I
hf : (ae (F := Measure ℝ) (Measure.restrict volume (Ioc (a i) (b i)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f a‖
hfi₁ : @Integrable ℝ _ _ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖f a‖) (Measure.restrict volume (Ioc (a i) (b i)))
hle : Ioc (a i) (b i) ∩ Ioc a₀ b₀ ⊆ Ioc (a i) (b i)
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc (a i) (b i) ∩ Ioc a₀ b₀)) fun (x : ℝ) ↦ ‖f x‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤
      I
i : ι
hi :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤ I
hf : ∀ (a : ℝ), LE.le (α := ℝ) (0 a) ((fun (a : ℝ) ↦ ‖f a‖) a)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioc (a i) (b i)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f a‖

Tactic:
apply ae_of_all

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤
      I
i : ι
hi :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤ I
⊢ ∀ (a : ℝ), LE.le (α := ℝ) (0 a) ((fun (a : ℝ) ↦ ‖f a‖) a)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤
      I
i : ι
hi :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤ I
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖f a‖) (Measure.restrict volume (Ioc (a i) (b i)))

Tactic:
(hfi i).norm

Premises used: MeasureTheory.Integrable.norm