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.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)
⊢ Integrable f μ
have refine : ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ ≤ I
Tactic: refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst : l.NeBot
inst_1 : l.IsCountablyGenerated
inst_2 : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ
ha : Tendsto a l atBot
hb : Tendsto b l atTop
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I
hφ : AECover μ l fun (i : ι) ↦ Ioc (a i) (b i)
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ ≤ I
have h₁ : ∀ (i : ι) (hai : a i ≤ 0) (hbi : 0 ≤ b i) (ht : ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I),
  ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ ≤ I
Tactic: filter_upwards [ha.eventually (eventually_le_atBot 0),
    hb.eventually (eventually_ge_atTop 0)] with i hai hbi ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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
⊢ IntegrableOn f (Iic b) μ
have hφ : AECover (μ.restrict (Iic b)) l fun (i : ι) ↦ Ioi (a i)
Tactic: have hφ : AECover (μ.restrict <| Iic b) l _ := aecover_Ioi ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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))
have rw : Integrable f (μ.restrict (Ioi (a i) ∩ Iic b))
Tactic: rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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)
⊢ IntegrableOn f (Iic b) μ
have hfi₁ : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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) μ
have refine : ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a x), ‖f x‖ ∂μ.restrict (Iic b) ≤ I
Tactic: refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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))
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a x), ‖f x‖ ∂μ.restrict (Iic b) ≤ I
have 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
Tactic: filter_upwards [ha.eventually (eventually_le_atBot b)] with i hai
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 a i..b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i), ‖f x‖ ∂μ.restrict (Iic b) ≤ I
have h₁ : ∫ (x : ℝ) in Ioc (a i) b, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi (a i) ∩ Iic b, ‖f x‖ ∂μ ≤ I
Tactic: rw [intervalIntegral.integral_of_le hai, Measure.restrict_restrict (hφ.measurableSet i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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
⊢ IntegrableOn f (Ioi a) μ
have hφ : AECover (μ.restrict (Ioi a)) l fun (i : ι) ↦ Iic (b i)
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.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))
have rw : Integrable f (μ.restrict (Ioi a ∩ Iic (b i)))
Tactic: rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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)
⊢ IntegrableOn f (Ioi a) μ
have hfi₁ : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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) μ
have refine : ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
Tactic: refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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))
⊢ ∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b x), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
have 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
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.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 a..b i, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Iic (b i), ‖f x‖ ∂μ.restrict (Ioi a) ≤ I
have h₁ : ∫ (x : ℝ) in Ioc a (b i), ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioi a ∩ Iic (b i), ‖f x‖ ∂μ ≤ I
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
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
have 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
Tactic: refine (aecover_Ioc_of_Ioc ha hb).integrable_of_integral_norm_bounded I
    (fun i => (hfi i).restrict) (h.mono fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict (Measure.restrict volume (Ioc a₀ b₀)) (Ioc (a i) (b i)))
      fun (x : ℝ) ↦ ‖f x‖) ≤
    I
have rw : (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc (a i) (b i) ∩ Ioc a₀ b₀)) fun (x : ℝ) ↦ ‖f x‖) ≤ I
Tactic: rw [Measure.restrict_restrict measurableSet_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc (a i) (b i) ∩ Ioc a₀ b₀)) fun (x : ℝ) ↦ ‖f x‖) ≤
    I
have 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‖)
Tactic: grw [← hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ 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‖)
have hf : (ae (F := Measure ℝ) (Measure.restrict volume (Ioc (a i) (b i)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f a‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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‖
⊢ 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‖)
have hfi₁ : @Integrable ℝ _ _ _ Real.measurableSpace (fun (a : ℝ) ↦ ‖f a‖) (Measure.restrict volume (Ioc (a i) (b i)))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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)))
⊢ 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‖)
have hle : Ioc (a i) (b i) ∩ Ioc a₀ b₀ ⊆ Ioc (a i) (b i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioc (a i) (b i)))).EventuallyLE (β := ℝ) 0 fun (a : ℝ) ↦ ‖f a‖
have hf : ∀ (a : ℝ), LE.le (α := ℝ) (0 a) ((fun (a : ℝ) ↦ ‖f a‖) a)
Tactic: apply ae_of_all
-- 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 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)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
have hφ : AECover μ l φ
Tactic: have hφ : AECover μ l φ := aecover_Ioc ha 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 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 ∂μ))
have 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 ∂μ
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
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 φ
⊢ EventuallyEq.{u_1, u_2} (β := E) l (fun (i : ι) ↦ ∫ (x : ℝ) in φ i, f x ∂μ) fun (i : ι) ↦
    ∫ (x : ℝ) in a i..b i, f x ∂μ
have 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 ∂μ)
Tactic: filter_upwards [ha.eventually (eventually_le_atBot 0),
    hb.eventually (eventually_ge_atTop 0)] with i hai hbi
-- 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
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : (i : ι) → Set ℝ := fun (i : ι) ↦ Ioi (a i)
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))
have hφ : AECover (μ.restrict (Iic b)) l φ
Tactic: have hφ : AECover (μ.restrict <| Iic b) l φ := aecover_Ioi ha
-- 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
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 ∂μ))
have 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 ∂μ
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
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 φ
⊢ 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 ∂μ
have 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 ∂μ)
Tactic: filter_upwards [ha.eventually (eventually_le_atBot <| b)] with i hai
-- 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
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, f x ∂μ.restrict (Iic b)) (∫ (x : ℝ) in a i..b, f x ∂μ)
have h : Eq.{u_2 + 1} (α := E) (∫ (x : ℝ) in φ i ∩ Iic b, f x ∂μ) (∫ (x : ℝ) in Ioc (a i) b, f x ∂μ)
Tactic: rw [intervalIntegral.integral_of_le hai, Measure.restrict_restrict (hφ.measurableSet i)]
-- 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 Iic (a i), f x ∂μ) l (𝓝 0)
have pos : ∀ (h : ∀ (b : ℝ), ¬IntegrableOn f (Iic b) μ),
  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) μ
-- 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 (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)
have neg : ∀ (h : ∃ (b : ℝ), IntegrableOn f (Iic b) μ),
  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) μ
-- 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 (Iic b) μ
⊢ Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)
have neg : ∀ (b : ℝ) (hb : IntegrableOn f (Iic b) μ),
  Tendsto.{u_1, u_2} (β := E) (fun (i : ι) ↦ ∫ (x : ℝ) in Iic (a i), f x ∂μ) l (𝓝 0)
Tactic: obtain ⟨b, hb⟩ := h
Cleared hypotheses: h