awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ 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 : ℝ | (fun (x : ℝ) ↦ indicator {t : ℝ | t ≤ x} f x₀ = 0) x} ∈ 𝓝 b₀
have h : ∀ x < x₀, indicator {t : ℝ | t ≤ x} f x₀ = 0
Tactic: apply Eventually.mono (Iio_mem_nhds hx₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
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₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
have this₁ : ∀ᶠ (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]
-- 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₁ 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
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
have refine_3 : indicator {t : ℝ | t ≤ b₀} f x₀ = 0
Tactic: apply continuousWithinAt_const.congr_of_eventuallyEq 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₀ 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₂
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
have neg : b₀ ∉ closure (Icc b₁ b₂)
Tactic: apply continuousWithinAt_of_notMem_closure
-- 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∞)
⊢ ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
have hsub : ∀ {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)
-- 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
⊢ ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
have Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Tactic: have Ioo_nhds : Ioo a b ∈ 𝓝 b₀ := Ioo_mem_nhds hb₀.1 hb₀.2
-- 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₀
⊢ ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
have Icc_nhds : Icc a b ∈ 𝓝 b₀
Tactic: have Icc_nhds : Icc a b ∈ 𝓝 b₀ := Icc_mem_nhds hb₀.1 hb₀.2
-- 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₀
⊢ ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
have hx₀ : ∀ᵐ (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
-- 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
⊢ ∀ᶠ (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 ∂μ
have 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 ∂μ
Tactic: rw [nhds_prod_eq]
-- 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
⊢ ∀ᶠ (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 ∂μ
have 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 ∂μ
Tactic: refine (h_bound.prod_mk Ioo_nhds).mono ?_
-- 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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
⊢ ∫ (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 ∂μ
have 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 ∂μ
Tactic: dsimp
-- 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
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
⊢ ∫ (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 ∂μ
have 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₀
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)
-- 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
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₀
⊢ ∫ (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 ∂μ
have hab : IntervalIntegrable (F x) μ a₀ b₀
Tactic: rw [intervalIntegral.integral_sub, add_assoc, add_sub_cancel,
      intervalIntegral.integral_add_adjacent_intervals]
-- 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
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₀
⊢ ∫ (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 ∂μ
have hbc : IntervalIntegrable (F x) μ b₀ t
Tactic: rw [intervalIntegral.integral_sub, add_assoc, add_sub_cancel,
      intervalIntegral.integral_add_adjacent_intervals]
-- 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
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
⊢ ∫ (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 ∂μ
have hg : IntervalIntegrable (F x₀) μ b₀ t
Tactic: rw [intervalIntegral.integral_sub, add_assoc, add_sub_cancel,
      intervalIntegral.integral_add_adjacent_intervals]
-- 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
⊢ ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
have this : ∀ᶠ (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: have : ∀ᶠ p : X × ℝ in 𝓝 (x₀, b₀),
      ∫ s in a₀..p.2, F p.1 s ∂μ =
        ∫ 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 ∂μ := 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⟩
    dsimp
    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)
    rw [intervalIntegral.integral_sub, add_assoc, add_sub_cancel,
      intervalIntegral.integral_add_adjacent_intervals]
    · exact hiF hx ha₀ hb₀
    · exact hiF hx hb₀ ht
    · exact hiF hx hb₀ ht
    · exact hiF hx₀ hb₀ ht
-- 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₀),
    ∫ (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 ∂μ
⊢ ContinuousAt.{u_2, u_1} (Y := E) (fun (p : X × ℝ) ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
have rw : ContinuousAt.{u_2, u_1} (Y := E)
  (fun (x : X × ℝ) ↦
    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 ∂μ)
  (x₀, b₀)
Tactic: rw [continuousAt_congr this]
-- 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
⊢ ContinuousAt.{u_2, u_1} (Y := E)
    (fun (x : X × ℝ) ↦
      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 ∂μ)
    (x₀, b₀)
have refine_1 : ContinuousAt.{u_2, u_1} (Y := E) (fun (x : X × ℝ) ↦ ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ) (x₀, b₀)
Tactic: refine (ContinuousAt.add ?_ ?_).add ?_
-- 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
refine_1 : ContinuousAt.{u_2, u_1} (Y := E) (fun (x : X × ℝ) ↦ ∫ (s : ℝ) in a₀..b₀, F x.1 s ∂μ) (x₀, b₀)
⊢ ContinuousAt.{u_2, u_1} (Y := E)
    (fun (x : X × ℝ) ↦
      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 ∂μ)
    (x₀, b₀)
have refine_2 : ContinuousAt.{u_2, u_1} (Y := E) (fun (x : X × ℝ) ↦ ∫ (s : ℝ) in b₀..x.2, F x₀ s ∂μ) (x₀, b₀)
Tactic: refine (ContinuousAt.add ?_ ?_).add ?_