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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
apply : ∀ (x_1 : ℝ), ‖F x x_1‖ ≤ bound x_1 ∧ ‖F x₀ x_1‖ ≤ bound x_1 → ‖F x x_1 - F x₀ x_1‖ ≤ 2 * bound x_1
⊢ ∀ᵐ (t : ℝ) ∂μ.restrict (Ι b₀ t), ‖F x t - F x₀ t‖ ≤ 2 * bound t

Tactic:
apply (ae_restrict_of_ae_restrict_of_subset (hsub hb₀ ht) (hx.and hx₀)).mono

Premises used: Filter.Eventually.and, Filter.Eventually.mono, MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- 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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
s : ℝ
hs₁ : ‖F x s‖ ≤ bound s
hs₂ : ‖F x₀ s‖ ≤ bound s
⊢ ‖F x s - F x₀ s‖ ≤ ‖F x s‖ + ‖F x₀ s‖

Tactic:
norm_sub_le _ _

Premises used: norm_sub_le
-- 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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
s : ℝ
hs₁ : ‖F x s‖ ≤ bound s
hs₂ : ‖F x₀ s‖ ≤ bound s
linarith :
  2 * bound s < ‖F x s‖ + ‖F x₀ s‖ → 2 * bound s - (‖F x s‖ + ‖F x₀ s‖) + (‖F x s‖ - bound s) + (‖F x₀ s‖ - bound s) = 0
⊢ ‖F x s‖ + ‖F x₀ s‖ ≤ 2 * bound s

Tactic:
linarith only [hs₁, hs₂]
-- 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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
s : ℝ
hs₁ : ‖F x s‖ ≤ bound s
hs₂ : ‖F x₀ s‖ ≤ bound s
x₁ : ‖F x s‖ + ‖F x₀ s‖ ≤ 2 * bound s
⊢ ‖F x s - F x₀ s‖ ≤ 2 * bound s

Tactic:
calc
          ‖F x s - F x₀ s‖ ≤ ‖F x s‖ + ‖F x₀ s‖ := norm_sub_le _ _
          _ ≤ 2 * bound s := by linarith only [hs₁, hs₂]

Premises used: norm_sub_le
-- 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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
⊢ ∀ᵐ (t : ℝ) ∂μ.restrict (Ι b₀ t), ‖F x t - F x₀ t‖ ≤ 2 * bound t

Tactic:
have H : ∀ᵐ t : ℝ ∂μ.restrict (Ι b₀ t), ‖F x t - F x₀ t‖ ≤ 2 * bound t := by
        apply (ae_restrict_of_ae_restrict_of_subset (hsub hb₀ ht) (hx.and hx₀)).mono
        rintro s ⟨hs₁, hs₂⟩
        calc
          ‖F x s - F x₀ s‖ ≤ ‖F x s‖ + ‖F x₀ s‖ := norm_sub_le _ _
          _ ≤ 2 * bound s := by linarith only [hs₁, hs₂]
-- 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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
H : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι b₀ t), ‖F x t - F x₀ t‖ ≤ 2 * bound t
⊢ norm.{u_1} (E := E) (∫ (s : ℝ) in b₀..(x, t).2, F (x, t).1 s - F x₀ s ∂μ) ≤
    |∫ (s : ℝ) in b₀..(x, t).2, 2 * bound s ∂μ|

Tactic:
intervalIntegral.norm_integral_le_abs_of_norm_le H
        ((bound_integrable.mono_set' <| hsub hb₀ ht).const_mul 2)

Premises used: IntervalIntegrable.mono_set', OfNat.ofNat, intervalIntegral.norm_integral_le_abs_of_norm_le, IntervalIntegrable.const_mul
-- 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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
H : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι b₀ t), ‖F x t - F x₀ t‖ ≤ 2 * bound t
⊢ norm.{u_1} (E := E) (∫ (s : ℝ) in b₀..(x, t).2, F (x, t).1 s - F x₀ s ∂μ) ≤
    |∫ (s : ℝ) in b₀..(x, t).2, 2 * bound s ∂μ|

Tactic:
exact intervalIntegral.norm_integral_le_abs_of_norm_le H
        ((bound_integrable.mono_set' <| hsub hb₀ ht).const_mul 2)

Premises used: IntervalIntegrable.mono_set', OfNat.ofNat, intervalIntegral.norm_integral_le_abs_of_norm_le, IntervalIntegrable.const_mul
-- 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
⊢ ∀ᶠ (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 ∂μ|

Tactic:
have : ∀ᶠ p : X × ℝ in 𝓝 (x₀, b₀),
        ‖∫ s in b₀..p.2, F p.1 s - F x₀ s ∂μ‖ ≤ |∫ s in b₀..p.2, 2 * bound s ∂μ| := by
      rw [nhds_prod_eq]
      refine (h_bound.prod_mk Ioo_nhds).mono ?_
      rintro ⟨x, t⟩ ⟨hx : ∀ᵐ t ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t, ht : t ∈ Ioo a b⟩
      have H : ∀ᵐ t : ℝ ∂μ.restrict (Ι b₀ t), ‖F x t - F x₀ t‖ ≤ 2 * bound t := by
        apply (ae_restrict_of_ae_restrict_of_subset (hsub hb₀ ht) (hx.and hx₀)).mono
        rintro s ⟨hs₁, hs₂⟩
        calc
          ‖F x s - F x₀ s‖ ≤ ‖F x s‖ + ‖F x₀ s‖ := norm_sub_le _ _
          _ ≤ 2 * bound s := by linarith only [hs₁, hs₂]
      exact intervalIntegral.norm_integral_le_abs_of_norm_le H
        ((bound_integrable.mono_set' <| hsub hb₀ ht).const_mul 2)
-- 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 :
  ∀ᶠ (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 ∂μ|
refine_3 : Tendsto (β := ℝ) (fun (n : X × ℝ) ↦ |∫ (s : ℝ) in b₀..n.2, 2 * bound s ∂μ|) (𝓝 (x₀, b₀)) (𝓝 0)
⊢ Tendsto.{u_2, u_1} (β := E) (fun (x : X × ℝ) ↦ ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ) (𝓝 (x₀, b₀)) (𝓝 0)

Tactic:
apply squeeze_zero_norm' this

Premises used: squeeze_zero_norm'
-- 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 : ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) b₀
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) (𝓝 b₀) (𝓝 0)

Tactic:
simpa [ContinuousAt] using this

Premises used: 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 : 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 ∂μ|
suffices : ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) b₀
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) (𝓝 b₀) (𝓝 0)

Tactic:
suffices ContinuousAt (fun t ↦ ∫ s in b₀..t, 2 * bound s ∂μ) b₀ by
        simpa [ContinuousAt] using this
-- 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 :
  ∀ᶠ (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 ∂μ|
apply : ContinuousWithinAt (Y := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) (Icc a b) b₀
⊢ ContinuousAt (Y := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) b₀

Tactic:
apply ContinuousWithinAt.continuousAt _ Icc_nhds

Premises used: ContinuousWithinAt.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 : 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 ∂μ|
apply : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2 * bound x) μ (min b₀ a) (max b₀ b)
⊢ ContinuousWithinAt (Y := ℝ) (fun (t : ℝ) ↦ ∫ (s : ℝ) in b₀..t, 2 * bound s ∂μ) (Icc a b) b₀

Tactic:
apply intervalIntegral.continuousWithinAt_primitive hμb₀

Premises used: intervalIntegral.continuousWithinAt_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 : 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 : IntervalIntegrable bound μ (min b₀ a) (max b₀ b)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 2 * bound x) μ (min b₀ a) (max b₀ b)

Tactic:
apply IntervalIntegrable.const_mul

Premises used: IntervalIntegrable.const_mul
-- 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 :
  ∀ᶠ (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 : Ι (min b₀ a) (max b₀ b) ⊆ Ι a b
⊢ IntervalIntegrable bound μ (min b₀ a) (max b₀ b)

Tactic:
apply bound_integrable.mono_set'

Premises used: IntervalIntegrable.mono_set'
-- 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 :
  ∀ᶠ (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
hf₁ hf₂ : Ι a b ⊆ Ι a b
⊢ Ι (min b₀ a) (max b₀ b) ⊆ Ι a b

Tactic:
rw [min_eq_right hb₀.1.le, max_eq_right hb₀.2.le]

Premises used: LT.lt.le, min_eq_right, max_eq_right, And.right, And.left
-- 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 :
  ∀ᶠ (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 (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]
-- 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)
refine_3 : Tendsto (β := ℝ) (fun (n : X × ℝ) ↦ |∫ (s : ℝ) in b₀..n.2, 2 * bound s ∂μ|) (𝓝 x₀ ×ˢ 𝓝 b₀) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : X × ℝ) ↦ |∫ (s : ℝ) in b₀..n.2, 2 * bound s ∂μ|) (𝓝 (x₀, b₀)) (𝓝 0)

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq