awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (hfi i).norm

Premises used: MeasureTheory.Integrable.norm
-- 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
⊢ Ioc (a i) (b i) ∩ Ioc a₀ b₀ ⊆ Ioc (a i) (b i)

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- 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
⊢ Ioc (a i) (b i) ∩ Ioc a₀ b₀ ⊆ Ioc (a i) (b i)

Tactic:
exact inter_subset_left

Premises used: Set.inter_subset_left
-- 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 : ι → ℝ
f : ℝ → E
I a₀ b : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc (a i) b) volume
ha : Tendsto a l (𝓝 a₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (a i) b)) fun (x : ℝ) ↦ ‖f x‖) ≤ I
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioc a₀ b) volume

Tactic:
integrableOn_Ioc_of_intervalIntegral_norm_bounded hfi ha tendsto_const_nhds h

Premises used: tendsto_const_nhds, MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded
-- 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
b : ι → ℝ
f : ℝ → E
I a b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn (mα := Real.measurableSpace) f (Ioc a (b i)) volume
hb : Tendsto b l (𝓝 b₀)
h :
  ∀ᶠ (i : ι) in l,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a (b i))) fun (x : ℝ) ↦ ‖f x‖) ≤ I
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioc a b₀) volume

Tactic:
integrableOn_Ioc_of_intervalIntegral_norm_bounded hfi tendsto_const_nhds hb h

Premises used: tendsto_const_nhds, MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded
-- 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 b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioc (a i) (b i)
⊢ AECover μ l φ

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.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioc (a i) (b i)
hφ : AECover μ l φ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), 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
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioc (a i) (b i)
hφ : AECover μ l φ
refine :
  EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in φ i, f x ∂μ) fun (i : ι) ↦
    ∫ (x : ℝ) in a i..b i, f x ∂μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), 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
a b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioc (a i) (b i)
hφ : AECover μ l φ
h :
  ∀ (i : ι) (hai : a i ≤ 0) (hbi : 0 ≤ b i),
    Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in φ i, f x ∂μ) (∫ (x : ℝ) in a i..b i, f x ∂μ)
⊢ EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in φ i, f x ∂μ) fun (i : ι) ↦
    ∫ (x : ℝ) in a i..b i, f x ∂μ

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

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

Tactic:
(intervalIntegral.integral_of_le (hai.trans hbi)).symm

Premises used: intervalIntegral.integral_of_le, LE.le.trans, 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 b : ι → ℝ
f : ℝ → E
hfi : Integrable f μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioc (a i) (b i)
hφ : AECover μ l φ
i : ι
hai : a i ≤ 0
hbi : 0 ≤ b i
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in φ i, f x ∂μ) (∫ (x : ℝ) in a i..b i, f x ∂μ)

Tactic:
exact (intervalIntegral.integral_of_le (hai.trans hbi)).symm

Premises used: intervalIntegral.integral_of_le, LE.le.trans, 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
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioi (a i)
⊢ AECover (μ.restrict (Iic b)) l φ

Tactic:
have hφ : AECover (μ.restrict <| Iic b) l φ := aecover_Ioi ha
-- 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 (Iic b) μ
ha : Tendsto a l atBot
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, 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
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
refine :
  EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b)) fun (i : ι) ↦
    ∫ (x : ℝ) in a i..b, f x ∂μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, 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
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
h :
  ∀ (i : ι) (hai : a i ≤ b),
    Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b)) (∫ (x : ℝ) in a i..b, f x ∂μ)
⊢ EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b)) fun (i : ι) ↦
    ∫ (x : ℝ) in a i..b, f x ∂μ

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

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.IsCountablyGenerated
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
i : ι
hai : a i ≤ b
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in φ i ∩ Iic b, f x ∂μ) (∫ (x : ℝ) in Ioc (a i) b, 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
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
pos :
  ∀ (h : ∀ (b : ℝ), ¬IntegrableOn f (Iic b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)
neg :
  ∀ (h : ∃ (b : ℝ), IntegrableOn f (Iic b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)

Tactic:
by_cases! h : ∀ b, ¬ IntegrableOn f (Iic 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 atBot
h : ∀ (b : ℝ), ¬IntegrableOn f (Iic b) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (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 atBot
h : ∀ (b : ℝ), ¬IntegrableOn f (Iic b) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (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 atBot
h : ∃ (b : ℝ), IntegrableOn f (Iic b) μ
neg :
  ∀ (b : ℝ) (hb : IntegrableOn f (Iic b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (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 atBot
b : ℝ
hb : IntegrableOn f (Iic b) μ
h :
  ∀ (i : ι) (hi : a i ∈ Iic b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ
⊢ ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ

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

Premises used: Filter.Tendsto.eventually_mem, Filter.Iic_mem_atBot
-- 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 (Iic b) μ
i : ι
hi : a i ∈ Iic b
h : HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic (a i), f x ∂μ) = ∫ (x : ℝ) in a i..b, f x ∂μ
h₁ h₂ : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in a i..b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ

Tactic:
rw [sub_eq_iff_comm,
      intervalIntegral.integral_Iic_sub_Iic (hb.mono_set (Iic_subset_Iic.2 hi)) hb]

Premises used: Iff.mpr, Set.Iic_subset_Iic, sub_eq_iff_comm, intervalIntegral.integral_Iic_sub_Iic, MeasureTheory.IntegrableOn.mono_set
-- 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 (Iic b) μ
⊢ ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ

Tactic:
have : ∀ᶠ i in l, ∫ x in Iic b, f x ∂μ - ∫ x in a i..b, f x ∂μ = ∫ x in Iic (a i), f x ∂μ := by
    filter_upwards [ha.eventually_mem (Iic_mem_atBot b)] with i hi
    rw [sub_eq_iff_comm,
      intervalIntegral.integral_Iic_sub_Iic (hb.mono_set (Iic_subset_Iic.2 hi)) 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
a : ι → ℝ
f : ℝ → E
ha : Tendsto a l atBot
b : ℝ
hb : IntegrableOn f (Iic b) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ
neg :
  Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic b, f x ∂μ)))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)

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

Premises used: sub_self, MeasureTheory.Measure.restrict, MeasureTheory.integral, Set.Iic
-- 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 (Iic b) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic b, f x ∂μ)))

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

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Iic, 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 (Iic b) μ
this :
  ∀ᶠ (i : ι) in l,
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l
    (𝓝 (HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic b, f x ∂μ)))

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

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Iic, 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 (Iio b) μ
ha : Tendsto a l atBot
⊢ EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in Ico (a i) b, f x ∂μ.restrict (Iio b)) fun (i : ι) ↦
    ∫ (x : ℝ) in Ico (a i) b, 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 atBot
pos :
  ∀ (h : ∀ (b : ℝ), ¬IntegrableOn f (Iio b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
neg :
  ∀ (h : ∃ (b : ℝ), IntegrableOn f (Iio b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)

Tactic:
by_cases! h : ∀ b, ¬ IntegrableOn f (Iio 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 atBot
h : ∀ (b : ℝ), ¬IntegrableOn f (Iio b) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (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 atBot
h : ∀ (b : ℝ), ¬IntegrableOn f (Iio b) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (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 atBot
h : ∃ (b : ℝ), IntegrableOn f (Iio b) μ
neg :
  ∀ (b : ℝ) (hb : IntegrableOn f (Iio b) μ),
    Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (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 atBot
b : ℝ
hb : IntegrableOn f (Iio b) μ
h :
  ∀ (i : ι) (hi : a i ∈ Iic b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ) = ∫ (x : ℝ) in Iio (a i), f x ∂μ
⊢ ∀ᶠ (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 ∂μ

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

Premises used: Filter.Tendsto.eventually_mem, Filter.Iic_mem_atBot
-- 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) μ
i : ι
hi : a i ∈ Iic b
h : HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio (a i), f x ∂μ) = ∫ (x : ℝ) in Ico (a i) b, f x ∂μ
h₁ h₂ : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ) = ∫ (x : ℝ) in Iio (a i), f x ∂μ

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

Premises used: sub_eq_iff_comm, intervalIntegral.integral_Iio_sub_Iio
-- 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) μ
⊢ ∀ᶠ (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 ∂μ

Tactic:
have : ∀ᶠ i in l, ∫ x in Iio b, f x ∂μ - ∫ x in Ico (a i) b, f x ∂μ =
      ∫ x in Iio (a i), f x ∂μ := by
    filter_upwards [ha.eventually_mem (Iic_mem_atBot b)] with i hi
    rw [sub_eq_iff_comm, intervalIntegral.integral_Iio_sub_Iio 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 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 ∂μ
neg :
  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 ∂μ)))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)

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

Premises used: sub_self, MeasureTheory.Measure.restrict, MeasureTheory.integral, Set.Iio