awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ
have 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 ∂μ
Tactic: filter_upwards [ha.eventually_mem (Iic_mem_atBot b)] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ
have h : HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic (a i), f x ∂μ) = ∫ (x : ℝ) in a i..b, f x ∂μ
Tactic: rw [sub_eq_iff_comm,
      intervalIntegral.integral_Iic_sub_Iic (hb.mono_set (Iic_subset_Iic.2 hi)) hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ) = ∫ (x : ℝ) in Iic (a i), f x ∂μ
have h₁ : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in a i..b, f x ∂μ) (∫ (x : ℝ) in a i..b, f x ∂μ)
Tactic: rw [sub_eq_iff_comm,
      intervalIntegral.integral_Iic_sub_Iic (hb.mono_set (Iic_subset_Iic.2 hi)) hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)
have 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 ∂μ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)
have 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 ∂μ)))
Tactic: rw [← sub_self (∫ x in Iic b, f x ∂μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
have pos : ∀ (h : ∀ (b : ℝ), ¬IntegrableOn f (Iio b) μ),
  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) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
have neg : ∀ (h : ∃ (b : ℝ), IntegrableOn f (Iio b) μ),
  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) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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)
have neg : ∀ (b : ℝ) (hb : IntegrableOn f (Iio b) μ),
  Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
Tactic: obtain ⟨b, hb⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ
have 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 ∂μ
Tactic: filter_upwards [ha.eventually_mem (Iic_mem_atBot b)] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ) = ∫ (x : ℝ) in Iio (a i), f x ∂μ
have 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 ∂μ
Tactic: rw [sub_eq_iff_comm, intervalIntegral.integral_Iio_sub_Iio hb hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ) = ∫ (x : ℝ) in Iio (a i), f x ∂μ
have h₁ : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ) (∫ (x : ℝ) in Ico (a i) b, f x ∂μ)
Tactic: rw [sub_eq_iff_comm, intervalIntegral.integral_Iio_sub_Iio hb hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
have 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 ∂μ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iio (a i), f x ∂μ) l (𝓝 0)
have 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 ∂μ)))
Tactic: rw [← sub_self (∫ x in Iio b, f x ∂μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Ioi a, f x ∂μ))
have hφ : AECover (μ.restrict (Ioi a)) l φ
Tactic: have hφ : AECover (μ.restrict <| Ioi a) l φ := aecover_Iic hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ))
have 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 ∂μ
Tactic: refine (hφ.integral_tendsto_of_countably_generated hfi).congr' ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 φ
⊢ 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 ∂μ
have 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 ∂μ)
Tactic: filter_upwards [hb.eventually (eventually_ge_atTop <| a)] with i hbi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 φ i, f x ∂μ.restrict (Ioi a)) (∫ (x : ℝ) in a..b i, f x ∂μ)
have h : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ioi a ∩ φ i, f x ∂μ) (∫ (x : ℝ) in Ioc a (b i), f x ∂μ)
Tactic: rw [intervalIntegral.integral_of_le hbi, Measure.restrict_restrict (hφ.measurableSet i),
    inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)
have pos : ∀ (h : ∀ (a : ℝ), ¬IntegrableOn f (Ioi a) μ),
  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) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)
have neg : ∀ (h : ∃ (a : ℝ), IntegrableOn f (Ioi a) μ),
  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) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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)
have neg : ∀ (a : ℝ) (ha : IntegrableOn f (Ioi a) μ),
  Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)
Tactic: obtain ⟨a, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ
have 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 ∂μ
Tactic: filter_upwards [hb.eventually_mem (Ici_mem_atTop a)] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ
have h : ∫ (x : ℝ) in Ioi a, f x ∂μ = HAdd.hAdd (α := E) (∫ (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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in a..b i, f x ∂μ) = ∫ (x : ℝ) in Ioi (b i), f x ∂μ
have h₁ : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add',
      intervalIntegral.integral_interval_add_Ioi ha (ha.mono_set (Ioi_subset_Ioi hi))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)
have 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 ∂μ
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))]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ioi (b i), f x ∂μ) l (𝓝 0)
have 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 ∂μ)))
Tactic: rw [← sub_self (∫ x in Ioi a, f x ∂μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
have pos : ∀ (h : ∀ (b : ℝ), ¬IntegrableOn f (Ici b) μ),
  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) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
have neg : ∀ (h : ∃ (b : ℝ), IntegrableOn f (Ici b) μ),
  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) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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)
have neg : ∀ (b : ℝ) (hb : IntegrableOn f (Ici b) μ),
  Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
Tactic: obtain ⟨b, hb⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ
have 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 ∂μ
Tactic: filter_upwards [ha.eventually_mem (Ici_mem_atTop b)] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ
have 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 ∂μ
Tactic: rw [sub_eq_iff_comm, intervalIntegral.integral_Ici_sub_Ici hb hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) = ∫ (x : ℝ) in Ici (a i), f x ∂μ
have h₁ : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in Ico b (a i), f x ∂μ) (∫ (x : ℝ) in Ico b (a i), f x ∂μ)
Tactic: rw [sub_eq_iff_comm, intervalIntegral.integral_Ici_sub_Ici hb hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
have 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 ∂μ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Ici (a i), f x ∂μ) l (𝓝 0)
have 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 ∂μ)))
Tactic: rw [← sub_self (∫ x in Ici b, f x ∂μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ Tendsto f atTop (𝓝 (limUnder atTop f))
have suffices : ∃ (a : E), Tendsto f atTop (𝓝 a)
Tactic: suffices ∃ a, Tendsto f atTop (𝓝 a) from tendsto_nhds_limUnder this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ ∃ (a : E), Tendsto f atTop (𝓝 a)
have suffices : CauchySeq f
Tactic: suffices CauchySeq f from cauchySeq_tendsto_of_complete this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ CauchySeq f
have apply : ∀ (ε : ℝ) (εpos : ε > 0), ∃ (N : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε
Tactic: apply Metric.cauchySeq_iff'.2 (fun ε εpos ↦ ?_)