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.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iio b) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ) = ∫ (x : ℝ) in Iio (a i), f x ∂μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio b, f x ∂μ)))

Tactic:
Tendsto.congr' this (Tendsto.const_sub _ <| tendsto_integral_Ico_integral_Iio b hb ha)

Premises used: MeasureTheory.tendsto_integral_Ico_integral_Iio, Filter.Tendsto.const_sub, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iio b) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ) = ∫ (x : ℝ) in Iio (a i), f x ∂μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio b, f x ∂μ)))

Tactic:
exact Tendsto.congr' this (Tendsto.const_sub _ <| tendsto_integral_Ico_integral_Iio b hb ha)

Premises used: MeasureTheory.tendsto_integral_Ico_integral_Iio, Filter.Tendsto.const_sub, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Iic (b i)
⊢ AECover (μ.restrict (Ioi a)) l φ

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.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Iic (b i)
hφ : AECover (μ.restrict (Ioi a)) l φ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))

Tactic:
(hφ.integral_tendsto_of_countably_generated hfi).congr' ?_

Premises used: MeasureTheory.AECover.integral_tendsto_of_countably_generated, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Iic (b i)
hφ : AECover (μ.restrict (Ioi a)) l φ
refine :
  EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Ioi a)) fun (i : ι) ↦
    ∫ (x : ℝ) in a..b i, f x ∂μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))

Tactic:
refine (hφ.integral_tendsto_of_countably_generated hfi).congr' ?_

Premises used: MeasureTheory.AECover.integral_tendsto_of_countably_generated, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Iic (b i)
hφ : AECover (μ.restrict (Ioi a)) l φ
h :
  ∀ (i : ι) (hbi : a ≤ b i),
    Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in φ i, f x ∂μ.restrict (Ioi a)) (∫ (x : ℝ) in a..b i, f x ∂μ)
⊢ EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Ioi a)) fun (i : ι) ↦
    ∫ (x : ℝ) in a..b i, f x ∂μ

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.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Iic (b i)
hφ : AECover (μ.restrict (Ioi a)) l φ
i : ι
hbi : a ≤ b i
h : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ioi a ∩ φ i, f x ∂μ) (∫ (x : ℝ) in Ioc a (b i), f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in φ i, f x ∂μ.restrict (Ioi a)) (∫ (x : ℝ) in a..b i, f x ∂μ)

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.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
a : ℝ
hfi : IntegrableOn f (Ioi a) μ
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Iic (b i)
hφ : AECover (μ.restrict (Ioi a)) l φ
i : ι
hbi : a ≤ b i
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ioi a ∩ φ i, f x ∂μ) (∫ (x : ℝ) in Ioc a (b i), f x ∂μ)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
pos :
  ∀ (h : ∀ (a : ℝ), ¬IntegrableOn f (Ioi a) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)
neg :
  ∀ (h : ∃ (a : ℝ), IntegrableOn f (Ioi a) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)

Tactic:
by_cases! h : ∀ a, ¬ IntegrableOn f (Ioi a) μ
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
h : ∀ (a : ℝ), ¬IntegrableOn f (Ioi a) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)

Tactic:
tendsto_const_nhds.congr (fun i => (integral_undef (h (b i))).symm)

Premises used: tendsto_const_nhds, MeasureTheory.integral_undef, Filter.Tendsto.congr, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
h : ∀ (a : ℝ), ¬IntegrableOn f (Ioi a) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)

Tactic:
exact tendsto_const_nhds.congr (fun i => (integral_undef (h (b i))).symm)

Premises used: tendsto_const_nhds, MeasureTheory.integral_undef, Filter.Tendsto.congr, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
h : ∃ (a : ℝ), IntegrableOn f (Ioi a) μ
neg :
  ∀ (a : ℝ) (ha : IntegrableOn f (Ioi a) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)

Tactic:
obtain ⟨a, ha⟩ := h
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
a : ℝ
ha : IntegrableOn f (Ioi a) μ
h :
  ∀ (i : ι) (hi : b i ∈ Ici a),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ
⊢ ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ

Tactic:
filter_upwards [hb.eventually_mem (Ici_mem_atTop a)] with i hi

Premises used: Filter.Tendsto.eventually_mem, Filter.Ici_mem_atTop
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
a : ℝ
ha : IntegrableOn f (Ioi a) μ
i : ι
hi : b i ∈ Ici a
h : ∫ (x : ℝ) in Ioi a, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b i, f x ∂μ) (∫ (x : ℝ) in Ioi (b i), f x ∂μ)
h₁ h₂ : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ

Tactic:
rw [sub_eq_iff_eq_add',
      intervalIntegral.integral_interval_add_Ioi ha (ha.mono_set (Ioi_subset_Ioi hi))]

Premises used: MeasureTheory.IntegrableOn.mono_set, Set.Ioi_subset_Ioi, intervalIntegral.integral_interval_add_Ioi, sub_eq_iff_eq_add'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
a : ℝ
ha : IntegrableOn f (Ioi a) μ
⊢ ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ

Tactic:
have : ∀ᶠ i in l, ∫ x in Ioi a, f x ∂μ - ∫ x in a..b i, f x ∂μ = ∫ x in Ioi (b i), f x ∂μ := by
    filter_upwards [hb.eventually_mem (Ici_mem_atTop a)] with i hi
    rw [sub_eq_iff_eq_add',
      intervalIntegral.integral_interval_add_Ioi ha (ha.mono_set (Ioi_subset_Ioi hi))]
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
a : ℝ
ha : IntegrableOn f (Ioi a) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ
neg :
  Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)

Tactic:
rw [← sub_self (∫ x in Ioi a, f x ∂μ)]

Premises used: Set.Ioi, sub_self, MeasureTheory.Measure.restrict, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
a : ℝ
ha : IntegrableOn f (Ioi a) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)))

Tactic:
Tendsto.congr' this (Tendsto.const_sub _ <| intervalIntegral_tendsto_integral_Ioi a ha hb)

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Ioi, Filter.Tendsto.const_sub, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : ι → ℝ
f : ℝ → E
hb : Tendsto b l atTop
a : ℝ
ha : IntegrableOn f (Ioi a) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)))

Tactic:
exact Tendsto.congr' this (Tendsto.const_sub _ <| intervalIntegral_tendsto_integral_Ioi a ha hb)

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Ioi, Filter.Tendsto.const_sub, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Ici b) μ
ha : Tendsto a l atTop
⊢ EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in Ico b (a i), f x ∂μ.restrict (Ici b)) fun (i : ι) ↦
    ∫ (x : ℝ) in Ico b (a i), f x ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
pos :
  ∀ (h : ∀ (b : ℝ), ¬IntegrableOn f (Ici b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
neg :
  ∀ (h : ∃ (b : ℝ), IntegrableOn f (Ici b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)

Tactic:
by_cases! h : ∀ b, ¬ IntegrableOn f (Ici b) μ
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
h : ∀ (b : ℝ), ¬IntegrableOn f (Ici b) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)

Tactic:
tendsto_const_nhds.congr (fun i => (integral_undef (h (a i))).symm)

Premises used: tendsto_const_nhds, MeasureTheory.integral_undef, Filter.Tendsto.congr, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
h : ∀ (b : ℝ), ¬IntegrableOn f (Ici b) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)

Tactic:
exact tendsto_const_nhds.congr (fun i => (integral_undef (h (a i))).symm)

Premises used: tendsto_const_nhds, MeasureTheory.integral_undef, Filter.Tendsto.congr, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
h : ∃ (b : ℝ), IntegrableOn f (Ici b) μ
neg :
  ∀ (b : ℝ) (hb : IntegrableOn f (Ici b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)

Tactic:
obtain ⟨b, hb⟩ := h
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
b : ℝ
hb : IntegrableOn f (Ici b) μ
h :
  ∀ (i : ι) (hi : a i ∈ Ici b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ
⊢ ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ

Tactic:
filter_upwards [ha.eventually_mem (Ici_mem_atTop b)] with i hi

Premises used: Filter.Tendsto.eventually_mem, Filter.Ici_mem_atTop
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
b : ℝ
hb : IntegrableOn f (Ici b) μ
i : ι
hi : a i ∈ Ici b
h : HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ici (a i), f x ∂μ) = ∫ (x : ℝ) in Ico b (a i), f x ∂μ
h₁ h₂ : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ

Tactic:
rw [sub_eq_iff_comm, intervalIntegral.integral_Ici_sub_Ici hb hi]

Premises used: sub_eq_iff_comm, intervalIntegral.integral_Ici_sub_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
b : ℝ
hb : IntegrableOn f (Ici b) μ
⊢ ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ

Tactic:
have : ∀ᶠ i in l, ∫ x in Ici b, f x ∂μ - ∫ x in Ico b (a i), f x ∂μ =
      ∫ x in Ici (a i), f x ∂μ := by
    filter_upwards [ha.eventually_mem (Ici_mem_atTop b)] with i hi
    rw [sub_eq_iff_comm, intervalIntegral.integral_Ici_sub_Ici hb hi]
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
b : ℝ
hb : IntegrableOn f (Ici b) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ
neg :
  Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ)))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)

Tactic:
rw [← sub_self (∫ x in Ici b, f x ∂μ)]

Premises used: Set.Ici, sub_self, MeasureTheory.Measure.restrict, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
b : ℝ
hb : IntegrableOn f (Ici b) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ)))

Tactic:
Tendsto.congr' this (Tendsto.const_sub _ <| tendsto_integral_Ico_integral_Ici b hb ha)

Premises used: Filter.Tendsto.const_sub, Filter.Tendsto.congr', MeasureTheory.tendsto_integral_Ico_integral_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atTop
b : ℝ
hb : IntegrableOn f (Ici b) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ)))

Tactic:
exact Tendsto.congr' this (Tendsto.const_sub _ <| tendsto_integral_Ico_integral_Ici b hb ha)

Premises used: Filter.Tendsto.const_sub, Filter.Tendsto.congr', MeasureTheory.tendsto_integral_Ico_integral_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
suffices : ∃ (a : E), Tendsto f atTop (𝓝 a)
⊢ Tendsto f atTop (𝓝 (limUnder atTop f))

Tactic:
suffices ∃ a, Tendsto f atTop (𝓝 a) from tendsto_nhds_limUnder this
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
suffices : CauchySeq f
⊢ ∃ (a : E), Tendsto f atTop (𝓝 a)

Tactic:
suffices CauchySeq f from cauchySeq_tendsto_of_complete this
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
apply : ∀ (ε : ℝ) (εpos : ε > 0), ∃ (N : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε
⊢ CauchySeq f

Tactic:
apply Metric.cauchySeq_iff'.2 (fun ε εpos ↦ ?_)

Premises used: Iff.mpr, Metric.cauchySeq_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
h_anti : Antitone (β := Set ℝ) fun (n : ℕ) ↦ Ici (↑n : ℝ)
hfi :
  ∃ (i : ℕ), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑i : ℝ)) volume
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (⋂ (n : ℕ), Ici (↑n : ℝ)))
        fun (x : ℝ) ↦ ‖f' x‖))

Tactic:
apply tendsto_setIntegral_of_antitone (fun n ↦ measurableSet_Ici)

Premises used: MeasureTheory.tendsto_setIntegral_of_antitone, measurableSet_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
m n : ℕ
hmn : m ≤ n
⊢ LE.le (α := Set ℝ) ((fun (n : ℕ) ↦ (Ici (↑n : ℝ) : Set ℝ)) n) ((fun (n : ℕ) ↦ (Ici (↑n : ℝ) : Set ℝ)) m)

Tactic:
Ici_subset_Ici.2 (Nat.cast_le.mpr hmn)

Premises used: Iff.mpr, Set.Ici_subset_Ici, Nat.cast_le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
m n : ℕ
hmn : m ≤ n
⊢ LE.le (α := Set ℝ) ((fun (n : ℕ) ↦ (Ici (↑n : ℝ) : Set ℝ)) n) ((fun (n : ℕ) ↦ (Ici (↑n : ℝ) : Set ℝ)) m)

Tactic:
exact Ici_subset_Ici.2 (Nat.cast_le.mpr hmn)

Premises used: Iff.mpr, Set.Ici_subset_Ici, Nat.cast_le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
hfi :
  ∀ (n : ℕ) (hn : a < (↑n : ℝ)),
    ∃ (i : ℕ), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑i : ℝ)) volume
⊢ ∃ (i : ℕ), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑i : ℝ)) volume

Tactic:
rcases exists_nat_gt a with ⟨n, hn⟩

Premises used: exists_nat_gt