awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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)

Tactic:
(continuous_abs.tendsto' _ _ abs_zero).comp (this.comp tendsto_snd)

Premises used: abs, abs_zero, Continuous.tendsto', Filter.Tendsto.comp, continuous_abs, Filter.tendsto_snd
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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)

Tactic:
exact (continuous_abs.tendsto' _ _ abs_zero).comp (this.comp tendsto_snd)

Premises used: abs_zero, Continuous.tendsto', Filter.Tendsto.comp, continuous_abs, Filter.tendsto_snd
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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)
neg : ∀ (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)

Tactic:
by_cases h : a ≤ b
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
x : ℝ
x_in : x ∈ Icc a b
⊢ Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Ioc a x, f t ∂μ) (∫ (t : ℝ) in a..x, f t ∂μ)

Tactic:
simp_rw [integral_of_le x_in.1]

Premises used: intervalIntegral.integral_of_le, And.left
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
⊢ ∀ 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]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 ∂μ)
pos : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in 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)

Tactic:
rw [continuousOn_congr this]

Premises used: continuousOn_congr
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀ : ℝ
pos : x₀ ∈ Icc a b → ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀
⊢ x₀ ∈ Icc a b → ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀

Tactic:
continuousWithinAt_primitive (measure_singleton x₀) ?_

Premises used: intervalIntegral.continuousWithinAt_primitive, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
pos : IntervalIntegrable f μ (min a a) (max a b)
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in a..x, f t ∂μ) (Icc a b) x₀

Tactic:
refine continuousWithinAt_primitive (measure_singleton x₀) ?_

Premises used: intervalIntegral.continuousWithinAt_primitive, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
pos : IntegrableOn f (Ioc a b) μ
⊢ IntervalIntegrable f μ (min a a) (max a b)

Tactic:
simp only [intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right, h, min_self]

Premises used: min_self, intervalIntegrable_iff_integrableOn_Ioc_of_le, max_eq_right
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
⊢ IntegrableOn f (Ioc a b) μ

Tactic:
h_int.mono Ioc_subset_Icc_self le_rfl

Premises used: le_rfl, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
⊢ IntegrableOn f (Ioc a b) μ

Tactic:
exact h_int.mono Ioc_subset_Icc_self le_rfl

Premises used: le_rfl, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
neg : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) ∅
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)

Tactic:
rw [Icc_eq_empty h]

Premises used: Set.Icc_eq_empty
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 ∂μ) ∅

Tactic:
continuousOn_empty _

Premises used: continuousOn_empty
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 ∂μ) ∅

Tactic:
exact continuousOn_empty _

Premises used: continuousOn_empty
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 : ∀ (x : ℝ), Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Icc a x, f t ∂μ) (∫ (t : ℝ) in Ioc a x, f t ∂μ)
⊢ 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:
ext x
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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) μ
x : ℝ
⊢ Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Icc a x, f t ∂μ) (∫ (t : ℝ) in Ioc a x, f t ∂μ)

Tactic:
integral_Icc_eq_integral_Ioc

Premises used: MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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) μ
x : ℝ
⊢ Eq.{u_1 + 1} (α := E) (∫ (t : ℝ) in Icc a x, f t ∂μ) (∫ (t : ℝ) in Ioc a x, f t ∂μ)

Tactic:
exact integral_Icc_eq_integral_Ioc

Premises used: MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 ∂μ

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
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 ∂μ
rw : 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 Icc a x, f t ∂μ) (Icc a b)

Tactic:
rw [aux]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 Ioc a x, f t ∂μ) (Icc a b)

Tactic:
continuousOn_primitive h_int

Premises used: intervalIntegral.continuousOn_primitive
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 Ioc a x, f t ∂μ) (Icc a b)

Tactic:
exact continuousOn_primitive h_int

Premises used: intervalIntegral.continuousOn_primitive
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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

Tactic:
continuousWithinAt_primitive (measure_singleton _) ?_

Premises used: intervalIntegral.continuousWithinAt_primitive, MeasureTheory.NoAtoms.measure_singleton, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₂]]
refine : IntervalIntegrable f μ (min a (min b₁ b₂)) (max a (max b₁ b₂))
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) [[b₁, b₂]] x

Tactic:
refine continuousWithinAt_primitive (measure_singleton _) ?_

Premises used: intervalIntegral.continuousWithinAt_primitive, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₂]]
rw : IntervalIntegrable f μ (min b₁ b₂) (max b₁ b₂)
⊢ IntervalIntegrable f μ (min a (min b₁ b₂)) (max a (max b₁ b₂))

Tactic:
rw [min_eq_right ha.1, max_eq_right ha.2]

Premises used: min_eq_right, max_eq_right, And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 b₁ b₂) (max b₁ b₂)

Tactic:
simpa [intervalIntegrable_iff, uIoc] using h_int

Premises used: intervalIntegrable_iff, Set.uIoc
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 a..x, f t ∂μ) [[a, b]]

Tactic:
continuousOn_primitive_interval' h_int.intervalIntegrable left_mem_uIcc

Premises used: Set.left_mem_uIcc, MeasureTheory.IntegrableOn.intervalIntegrable, intervalIntegral.continuousOn_primitive_interval'
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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]] μ
rw :
  ∀ (h_int : IntegrableOn f [[b, a]] μ),
    ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in x..b, f t ∂μ) [[a, b]]

Tactic:
rw [uIcc_comm a b] at h_int ⊢

Premises used: Set.uIcc_comm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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]] μ
simp : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ -∫ (t : ℝ) in b..x, f t ∂μ) [[b, a]]
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ ∫ (t : ℝ) in x..b, f t ∂μ) [[b, a]]

Tactic:
simp only [integral_symm b]

Premises used: intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 b..x, f t ∂μ) [[b, a]]

Tactic:
(continuousOn_primitive_interval h_int).neg

Premises used: intervalIntegral.continuousOn_primitive_interval, ContinuousOn.neg
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 b..x, f t ∂μ) [[b, a]]

Tactic:
exact (continuousOn_primitive_interval h_int).neg

Premises used: intervalIntegral.continuousOn_primitive_interval, ContinuousOn.neg
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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 : ℝ
rw : ∀ (x : ℝ), ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) x
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀ : ℝ
obtain : ∀ (b₁ : ℝ) (hb₁ : b₁ < b₀), ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀

Tactic:
obtain ⟨b₁, hb₁⟩ := exists_lt b₀

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀
obtain : ∀ (b₂ : ℝ) (hb₂ : b₀ < b₂), ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀

Tactic:
obtain ⟨b₂, hb₂⟩ := exists_gt b₀

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₂
apply : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) b₀

Tactic:
apply ContinuousWithinAt.continuousAt _ (Icc_mem_nhds hb₁ hb₂)

Premises used: ContinuousWithinAt.continuousAt, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₂
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
continuousWithinAt_primitive (measure_singleton b₀) (h_int _ _)

Premises used: intervalIntegral.continuousWithinAt_primitive, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₂
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
exact continuousWithinAt_primitive (measure_singleton b₀) (h_int _ _)

Premises used: intervalIntegral.continuousWithinAt_primitive, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
h_int : Integrable f μ
a : ℝ
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
continuous_primitive (fun _ _ => h_int.intervalIntegrable) a

Premises used: MeasureTheory.Integrable.intervalIntegrable, intervalIntegral.continuous_primitive
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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)
rw : ∀ (x : X × ℝ), ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ) x
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : X × ℝ) ↦
    ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀ : ℝ
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 ∂μ) < ε
⊢ ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ) (q, b₀)

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

Premises used: Iff.mpr, Metric.continuousAt_iff'
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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
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 ∂μ) < ε
⊢ ∀ᶠ (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₀)

Premises used: NoMinOrder.exists_lt, Min.min
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
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₀
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 ∂μ) < ε
⊢ ∀ᶠ (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₀)

Premises used: NoMaxOrder.exists_gt, Max.max