awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt.{u_2, u_1} (Y := E) (fun (x : X) ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
this :
  ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀),
    norm.{u_1} (E := E) (∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ) ≤ |∫ (s : ℝ) in b₀..p.2, 2 * bound s ∂μ|
⊢ Ι (min b₀ a) (max b₀ b) ⊆ Ι a b
have hf : Ι a (max b₀ b) ⊆ Ι a b
Tactic: rw [min_eq_right hb₀.1.le, max_eq_right hb₀.2.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt.{u_2, u_1} (Y := E) (fun (x : X) ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
this :
  ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀),
    norm.{u_1} (E := E) (∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ) ≤ |∫ (s : ℝ) in b₀..p.2, 2 * bound s ∂μ|
hf : Ι a (max b₀ b) ⊆ Ι a b
⊢ Ι (min b₀ a) (max b₀ b) ⊆ Ι a b
have hf₁ : Ι a b ⊆ Ι a b
Tactic: rw [min_eq_right hb₀.1.le, max_eq_right hb₀.2.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt.{u_2, u_1} (Y := E) (fun (x : X) ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
this :
  ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀),
    norm.{u_1} (E := E) (∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ) ≤ |∫ (s : ℝ) in b₀..p.2, 2 * bound s ∂μ|
⊢ Tendsto (β := ℝ) (fun (n : X × ℝ) ↦ |∫ (s : ℝ) in b₀..n.2, 2 * bound s ∂μ|) (𝓝 (x₀, b₀)) (𝓝 0)
have this₁ : Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) (𝓝 b₀) (𝓝 0)
Tactic: have : Tendsto (fun t ↦ ∫ s in b₀..t, 2 * bound s ∂μ) (𝓝 b₀) (𝓝 0) := by
      suffices ContinuousAt (fun t ↦ ∫ s in b₀..t, 2 * bound s ∂μ) b₀ by
        simpa [ContinuousAt] using this
      apply ContinuousWithinAt.continuousAt _ Icc_nhds
      apply intervalIntegral.continuousWithinAt_primitive hμb₀
      apply IntervalIntegrable.const_mul
      apply bound_integrable.mono_set'
      rw [min_eq_right hb₀.1.le, max_eq_right hb₀.2.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt.{u_2, u_1} (Y := E) (fun (x : X) ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
this_1 :
  ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀),
    norm.{u_1} (E := E) (∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ) ≤ |∫ (s : ℝ) in b₀..p.2, 2 * bound s ∂μ|
this : Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) (𝓝 b₀) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : X × ℝ) ↦ |∫ (s : ℝ) in b₀..n.2, 2 * bound s ∂μ|) (𝓝 (x₀, b₀)) (𝓝 0)
have refine_3 : Tendsto (β := ℝ) (fun (n : X × ℝ) ↦ |∫ (s : ℝ) in b₀..n.2, 2 * bound s ∂μ|) (𝓝 x₀ ×ˢ 𝓝 b₀) (𝓝 0)
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
have pos : ∀ (h : a ≤ b), ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
pos : ∀ (h : a ≤ b), ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
have neg : ∀ (h : ¬a ≤ b), ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
have this : ∀ x ∈ Icc a b, Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Ioc a x, f t ∂μ) (∫ (t : ℝ) in a..x, f t ∂μ)
Tactic: have : ∀ x ∈ Icc a b, ∫ t in Ioc a x, f t ∂μ = ∫ t in a..x, f t ∂μ := by
      intro x x_in
      simp_rw [integral_of_le x_in.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Ioc a x, f t ∂μ) (∫ (t : ℝ) in a..x, f t ∂μ)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
have pos : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b)
Tactic: rw [continuousOn_congr this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Ioc a x, f t ∂μ) (∫ (t : ℝ) in a..x, f t ∂μ)
x₀ : ℝ
h_1 : x₀ ∈ Icc a b
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀
have pos : IntervalIntegrable f μ (min a a) (max a b)
Tactic: refine continuousWithinAt_primitive (measure_singleton x₀) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
this : ∀ x ∈ Icc a b, Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Ioc a x, f t ∂μ) (∫ (t : ℝ) in a..x, f t ∂μ)
x₀ : ℝ
h_1 : x₀ ∈ Icc a b
⊢ IntervalIntegrable f μ (min a a) (max a b)
have pos : IntegrableOn f (Ioc a b) μ
Tactic: simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right, h, min_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
h : ¬a ≤ b
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
have neg : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) ∅
Tactic: rw [Icc_eq_empty h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
⊢ Eq.{u_1 + 1} (α := (x : ℝ) → E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) fun (x : ℝ) ↦
    ∫ (t : ℝ) in Ioc a x, f t ∂μ
have h : ∀ (x : ℝ), Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Icc a x, f t ∂μ) (∫ (t : ℝ) in Ioc a x, f t ∂μ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)
have aux : Eq.{u_1 + 1} (α := (x : ℝ) → E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ
Tactic: have aux : (fun x => ∫ t in Icc a x, f t ∂μ) = fun x => ∫ t in Ioc a x, f t ∂μ := by
    ext x
    exact integral_Icc_eq_integral_Ioc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f (Icc a b) μ
aux :
  Eq.{u_1 + 1} (α := (x : ℝ) → E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) fun (x : ℝ) ↦
    ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)
have rw : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
Tactic: rw [aux]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x : ℝ
h : x ∈ [[b₁, b₂]]
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) [[b₁, b₂]] x
have refine : IntervalIntegrable f μ (min a (min b₁ b₂)) (max a (max b₁ b₂))
Tactic: refine continuousWithinAt_primitive (measure_singleton _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntervalIntegrable f μ b₁ b₂
ha : a ∈ [[b₁, b₂]]
x : ℝ
h : x ∈ [[b₁, b₂]]
⊢ IntervalIntegrable f μ (min a (min b₁ b₂)) (max a (max b₁ b₂))
have rw : IntervalIntegrable f μ (min b₁ b₂) (max b₁ b₂)
Tactic: rw [min_eq_right ha.1, max_eq_right ha.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f [[a, b]] μ
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in x..b, f t ∂μ) [[a, b]]
have rw : ∀ (h_int : IntegrableOn f [[b, a]] μ), ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]
Tactic: rw [uIcc_comm a b] at h_int ⊢
Cleared hypotheses: h_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : IntegrableOn f [[b, a]] μ
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]
have simp : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ -∫ (t : ℝ) in b..x, f t ∂μ) [[b, a]]
Tactic: simp only [integral_symm b]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a : ℝ
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ
have rw : ∀ (x : ℝ), ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ : ℝ
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀
have obtain : ∀ (b₁ : ℝ) (hb₁ : b₁ < b₀), ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀
Tactic: obtain ⟨b₁, hb₁⟩ := exists_lt b₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀
have obtain : ∀ (b₂ : ℝ) (hb₂ : b₀ < b₂), ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀
Tactic: obtain ⟨b₂, hb₂⟩ := exists_gt b₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀
have apply : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
Tactic: apply ContinuousWithinAt.continuousAt _ (Icc_mem_nhds hb₁ hb₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : X × ℝ) ↦
    ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ
have rw : ∀ (x : X × ℝ), ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ : ℝ
⊢ ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ) (q, b₀)
have apply : ∀ (ε : ℝ) (εpos : ε > 0),
  ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
Tactic: apply Metric.continuousAt_iff'.2 (fun ε εpos ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
have obtain : ∀ (a : ℝ) (a_lt : a < min a₀ b₀),
  ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
Tactic: obtain ⟨a, a_lt⟩ := exists_lt (min a₀ b₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < min a₀ b₀
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
have obtain : ∀ (b : ℝ) (lt_b : max a₀ b₀ < b),
  ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
Tactic: obtain ⟨b, lt_b⟩ := exists_gt (max a₀ b₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < min a₀ b₀
b : ℝ
lt_b : max a₀ b₀ < b
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
have rw : ∀ (a_lt : a < a₀ ∧ a < b₀) (b : ℝ) (lt_b : max a₀ b₀ < b),
  ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
Tactic: rw [lt_min_iff] at a_lt
Cleared hypotheses: a_lt, b, lt_b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : max a₀ b₀ < b
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
have lt_b₁ : a₀ < b ∧ b₀ < b
Tactic: rw [max_lt_iff] at lt_b
Cleared hypotheses: lt_b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
have this : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
Tactic: have : IsCompact ({q} ×ˢ (Icc a b)) := isCompact_singleton.prod isCompact_Icc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
have obtain : ∀ (M : ℝ)
  (hM :
    Membership.mem (γ := Set ℝ)
      (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M),
  ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist.{u_1} (α := E) (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
Tactic: obtain ⟨M, hM⟩ := this.bddAbove_image hf.norm.continuousOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
⊢ ∃ (δ : ℝ),
    0 < δ ∧
      δ < 1 ∧ Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b ∧ (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
have A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, Membership.mem (γ := Set ℝ) (Ioo 0 1) δ
Tactic: have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), δ ∈ Ioo 0 1 := Ioo_mem_nhdsGT zero_lt_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, Membership.mem (γ := Set ℝ) (Ioo 0 1) δ
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
have I : Tendsto (fun (δ : ℝ) ↦ b₀ - δ) (𝓝 0) (𝓝 (b₀ - 0))
Tactic: have I : Tendsto (fun δ ↦ b₀ - δ) (𝓝 0) (𝓝 (b₀ - 0)) := tendsto_const_nhds.sub tendsto_id
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, Membership.mem (γ := Set ℝ) (Ioo 0 1) δ
I : Tendsto (fun (δ : ℝ) ↦ b₀ - δ) (𝓝 0) (𝓝 (b₀ - 0))
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
have J : Tendsto (fun (δ : ℝ) ↦ b₀ + δ) (𝓝 0) (𝓝 (b₀ + 0))
Tactic: have J : Tendsto (fun δ ↦ b₀ + δ) (𝓝 0) (𝓝 (b₀ + 0)) := tendsto_const_nhds.add tendsto_id