awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
h : ∀ x < x₀, indicator {t : ℝ | t ≤ x} f x₀ = 0
⊢ {x : ℝ | (fun (x : ℝ) ↦ indicator {t : ℝ | t ≤ x} f x₀ = 0) x} ∈ 𝓝 b₀

Tactic:
apply Eventually.mono (Iio_mem_nhds hx₀)

Premises used: Iio_mem_nhds, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
x : ℝ
hx : x < x₀
⊢ indicator {t : ℝ | t ≤ x} f x₀ = 0

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = 0

Tactic:
have : ∀ᶠ x in 𝓝[Icc b₁ b₂] b₀, {t : ℝ | t ≤ x}.indicator f x₀ = 0 := by
          apply mem_nhdsWithin_of_mem_nhds
          apply Eventually.mono (Iio_mem_nhds hx₀)
          intro x hx
          simp [hx]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this_2 : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = 0
refine_3 : indicator {t : ℝ | t ≤ b₀} f x₀ = 0
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀

Tactic:
apply continuousWithinAt_const.congr_of_eventuallyEq this

Premises used: ContinuousWithinAt.congr_of_eventuallyEq, continuousWithinAt_const
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this_2 : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = 0
⊢ indicator {t : ℝ | t ≤ b₀} f x₀ = 0

Tactic:
simp [hx₀]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∉ Icc b₁ b₂
neg : b₀ ∉ closure (Icc b₁ b₂)
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
apply continuousWithinAt_of_notMem_closure

Premises used: continuousWithinAt_of_notMem_closure
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ neg neg₁ neg₂ neg₃ : b₀ ∉ Icc b₁ b₂
⊢ b₀ ∉ closure (Icc b₁ b₂)

Tactic:
rwa [closure_Icc]

Premises used: closure_Icc
-- 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∞)
⊢ ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b

Tactic:
have hsub : ∀ {a₀ b₀}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b := fun ha₀ hb₀ ↦
    (ordConnected_Ioo.uIoc_subset ha₀ hb₀).trans (Ioo_subset_Ioc_self.trans Ioc_subset_uIoc)
-- 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 a b ∈ 𝓝 b₀

Tactic:
have Ioo_nhds : Ioo a b ∈ 𝓝 b₀ := Ioo_mem_nhds hb₀.1 hb₀.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 a b ∈ 𝓝 b₀

Tactic:
have Icc_nhds : Icc a b ∈ 𝓝 b₀ := Icc_mem_nhds hb₀.1 hb₀.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₀
⊢ ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t

Tactic:
have hx₀ : ∀ᵐ t : ℝ ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t := h_bound.self_of_nhds
-- 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
rw :
  ∀ᶠ (p : X × ℝ) in 𝓝 x₀ ×ˢ 𝓝 b₀,
    ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ =
      HAdd.hAdd (α := E) (∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ) (∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ) +
        ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ
⊢ ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀),
    ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ =
      HAdd.hAdd (α := E) (∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ) (∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ) +
        ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- 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₀,
    ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ =
      HAdd.hAdd (α := E) (∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ) (∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ) +
        ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ

Tactic:
(h_bound.prod_mk Ioo_nhds).mono ?_

Premises used: Filter.Eventually.mono, Filter.Eventually.prod_mk
-- 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
refine :
  ∀ (x : X × ℝ),
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x.1 t‖ ≤ bound t) ∧ a < x.2 ∧ x.2 < b →
      ∫ (s : ℝ) in a₀..x.2, F x.1 s ∂μ =
        HAdd.hAdd (α := E) (∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ) (∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ) +
          ∫ (s : ℝ) in b₀..x.2, F x.1 s - F x₀ s ∂μ
⊢ ∀ᶠ (p : X × ℝ) in 𝓝 x₀ ×ˢ 𝓝 b₀,
    ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ =
      HAdd.hAdd (α := E) (∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ) (∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ) +
        ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ

Tactic:
refine (h_bound.prod_mk Ioo_nhds).mono ?_

Premises used: Filter.Eventually.mono, Filter.Eventually.prod_mk
-- 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
dsimp :
  ∫ (s : ℝ) in a₀..t, F x s ∂μ =
    HAdd.hAdd (α := E) (∫ (s : ℝ) in a₀..b₀, F x s ∂μ) (∫ (s : ℝ) in b₀..t, F x₀ s ∂μ) +
      ∫ (s : ℝ) in b₀..t, F x s - F x₀ s ∂μ
⊢ ∫ (s : ℝ) in a₀..(x, t).2, F (x, t).1 s ∂μ =
    HAdd.hAdd (α := E) (∫ (s : ℝ) in a₀..b₀, F (x, t).1 s ∂μ) (∫ (s : ℝ) in b₀..(x, t).2, F x₀ s ∂μ) +
      ∫ (s : ℝ) in b₀..(x, t).2, F (x, t).1 s - F x₀ s ∂μ

Tactic:
dsimp
-- 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
⊢ ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀

Tactic:
have hiF : ∀ {x a₀ b₀},
        (∀ᵐ t : ℝ ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b →
          IntervalIntegrable (F x) μ a₀ b₀ := fun {x a₀ b₀} hx ha₀ hb₀ ↦
      (bound_integrable.mono_set_ae <| Eventually.of_forall <| hsub ha₀ hb₀).mono_fun'
        ((hF_meas x).mono_set <| hsub ha₀ hb₀)
        (ae_restrict_of_ae_restrict_of_subset (hsub ha₀ hb₀) hx)
-- 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
hiF :
  ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀
hab : IntervalIntegrable (F x) μ a₀ b₀
hbc hf : IntervalIntegrable (F x) μ b₀ t
hg : IntervalIntegrable (F x₀) μ b₀ t
⊢ ∫ (s : ℝ) in a₀..t, F x s ∂μ =
    HAdd.hAdd (α := E) (∫ (s : ℝ) in a₀..b₀, F x s ∂μ) (∫ (s : ℝ) in b₀..t, F x₀ s ∂μ) +
      ∫ (s : ℝ) in b₀..t, F x s - F x₀ s ∂μ

Tactic:
rw [intervalIntegral.integral_sub, add_assoc, add_sub_cancel,
      intervalIntegral.integral_add_adjacent_intervals]

Premises used: add_assoc, intervalIntegral.integral_add_adjacent_intervals, intervalIntegral.integral_sub, add_sub_cancel
-- 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
hiF :
  ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀
⊢ IntervalIntegrable (F x) μ a₀ b₀

Tactic:
hiF hx ha₀ hb₀
-- 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
hiF :
  ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀
⊢ IntervalIntegrable (F x) μ a₀ b₀

Tactic:
exact hiF hx ha₀ hb₀
-- 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
hiF :
  ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀
⊢ IntervalIntegrable (F x) μ b₀ t

Tactic:
hiF hx hb₀ ht
-- 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
hiF :
  ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀
⊢ IntervalIntegrable (F x) μ b₀ t

Tactic:
exact hiF hx hb₀ ht
-- 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
hiF :
  ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀
⊢ IntervalIntegrable (F x₀) μ b₀ t

Tactic:
hiF hx₀ hb₀ ht
-- 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
hiF :
  ∀ {x : X} {a₀ b₀ : ℝ},
    (∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → IntervalIntegrable (F x) μ a₀ b₀
⊢ IntervalIntegrable (F x₀) μ b₀ t

Tactic:
exact hiF hx₀ hb₀ ht