awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
x_1 : ℝ
hx : x_1 ∈ Ι a b
x : ↥{ carrier := [[a, b]], isCompact' := ⋯ } :=
  Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Compacts ℝ) { carrier := [[a, b]], isCompact' := ⋯ } x) x_1 ⋯
⊢ Summable.{u_2, u_1} (α := C((↑(↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) : Type), E))
    fun (i : ι) ↦ ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ } : Set ℝ) (f i)

Tactic:
have := hf_sum.of_norm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
hE : CompleteSpace E
x_1 : ℝ
hx : x_1 ∈ Ι a b
x : ↥{ carrier := [[a, b]], isCompact' := ⋯ } :=
  Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Compacts ℝ) { carrier := [[a, b]], isCompact' := ⋯ } x) x_1 ⋯
this :
  Summable.{u_2, u_1} (α := C((↑(↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) : Type), E))
    fun (i : ι) ↦ ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ } : Set ℝ) (f i)
⊢ Summable.{u_2, u_1} (α := E) fun (n : ι) ↦ (f n : (a : ℝ) → E) x_1

Tactic:
simpa only [Compacts.coe_mk, ContinuousMap.restrict_apply]
      using ContinuousMap.summable_apply this x

Premises used: TopologicalSpace.Compacts.coe_mk, ContinuousMap.summable_apply, ContinuousMap.restrict_apply
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : Countable ι
f : ι → C(ℝ, E)
hf_sum :
  Summable (α := ℝ) fun (i : ι) ↦
    ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ : Compacts ℝ } : Set ℝ) (f i)‖
⊢ Eq.{u_2 + 1} (α := E) (∑' (i : ι), ∫ (x : ℝ) in a..b, (f i : (a : ℝ) → E) x)
    (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i : (a : ℝ) → E) x)

Tactic:
(hasSum_intervalIntegral_of_summable_norm hf_sum).tsum_eq

Premises used: intervalIntegral.hasSum_intervalIntegral_of_summable_norm, HasSum.tsum_eq
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → ℝ → E
x₀ : X
bound : ℝ → ℝ
a b : ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousWithinAt.{u_3, u_2} (Y := E) (fun (x : X) ↦ F x t) s x₀
⊢ ContinuousWithinAt.{u_3, u_2} (Y := E) (fun (x : X) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) s x₀

Tactic:
tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_cont

Premises used: ContinuousWithinAt, intervalIntegral.tendsto_integral_filter_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → ℝ → E
x₀ : X
bound : ℝ → ℝ
a b : ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousAt.{u_3, u_2} (Y := E) (fun (x : X) ↦ F x t) x₀
⊢ ContinuousAt.{u_3, u_2} (Y := E) (fun (x : X) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) x₀

Tactic:
tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_cont

Premises used: intervalIntegral.tendsto_integral_filter_of_dominated_convergence, ContinuousAt
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
X : Type u_3
inst_2 : TopologicalSpace X
inst_3 : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b : ℝ
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont :
  ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ F x t
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ ∫ (t : ℝ) in a..b, F x t ∂μ

Tactic:
continuous_iff_continuousAt.mpr fun _ =>
    continuousAt_of_dominated_interval (Eventually.of_forall hF_meas) (Eventually.of_forall h_bound)
        bound_integrable <|
      h_cont.mono fun _ himp hx => (himp hx).continuousAt

Premises used: Iff.mpr, intervalIntegral.continuousAt_of_dominated_interval, Filter.Eventually.of_forall, Filter.Eventually.mono, Continuous.continuousAt, continuous_iff_continuousAt
-- 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₂)
pos :
  ∀ (h₀ : b₀ ∈ Icc b₁ b₂), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
neg :
  ∀ (h₀ : b₀ ∉ Icc b₁ b₂), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
by_cases h₀ : b₀ ∈ Icc b₁ b₂

Premises used: Set.Icc
-- 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₂
⊢ b₁ ≤ b₂

Tactic:
have h₁₂ : b₁ ≤ b₂ := h₀.1.trans h₀.2
-- 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 b₁ b₂ = b₁

Tactic:
have min₁₂ : min b₁ b₂ = b₁ := min_eq_left h₁₂
-- 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₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
apply : [[b₁, x]] ⊆ [[min a b₁, max a b₂]]
⊢ IntervalIntegrable f μ b₁ x

Tactic:
apply h_int.mono_set

Premises used: IntervalIntegrable.mono_set
-- 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₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
h₃ : b₁ ∈ [[min a b₁, max a b₂]]
h₄ : x ∈ [[min a b₁, max a b₂]]
⊢ [[b₁, x]] ⊆ [[min a b₁, max a b₂]]

Tactic:
apply uIcc_subset_uIcc

Premises used: Set.uIcc_subset_uIcc
-- 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₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ b₁ ∈ [[min a b₁, max a b₂]]

Tactic:
⟨min_le_of_left_le (min_le_right a b₁),
          h₁.trans (h₂.trans <| le_max_of_le_right <| le_max_right _ _)⟩

Premises used: le_max_right, Set.Mem, setOf, min_le_of_left_le, Set.Icc, le_max_of_le_right, And.intro, min_le_right, LE.le.trans, Set.uIcc
-- 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₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ b₁ ∈ [[min a b₁, max a b₂]]

Tactic:
exact ⟨min_le_of_left_le (min_le_right a b₁),
          h₁.trans (h₂.trans <| le_max_of_le_right <| le_max_right _ _)⟩
-- 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₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ x ∈ [[min a b₁, max a b₂]]

Tactic:
⟨min_le_of_left_le <| (min_le_right _ _).trans h₁,
          le_max_of_le_right <| h₂.trans <| le_max_right _ _⟩

Premises used: le_max_right, Set.Mem, setOf, min_le_of_left_le, Set.Icc, le_max_of_le_right, And.intro, min_le_right, LE.le.trans, Set.uIcc
-- 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₁
x : ℝ
h₁ : b₁ ≤ x
h₂ : x ≤ b₂
⊢ x ∈ [[min a b₁, max a b₂]]

Tactic:
exact ⟨min_le_of_left_le <| (min_le_right _ _).trans h₁,
          le_max_of_le_right <| h₂.trans <| le_max_right _ _⟩
-- 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₁
⊢ ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x

Tactic:
have h_int' : ∀ {x}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x := by
      rintro x ⟨h₁, h₂⟩
      apply h_int.mono_set
      apply uIcc_subset_uIcc
      · exact ⟨min_le_of_left_le (min_le_right a b₁),
          h₁.trans (h₂.trans <| le_max_of_le_right <| le_max_right _ _)⟩
      · exact ⟨min_le_of_left_le <| (min_le_right _ _).trans h₁,
          le_max_of_le_right <| h₂.trans <| le_max_right _ _⟩
-- 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
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
rw : IntervalIntegrable f μ a b₁
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..b, f x ∂μ)

Tactic:
rw [← integral_add_adjacent_intervals _ (h_int' ⟨h₁, h₂⟩)]

Premises used: intervalIntegral.integral_add_adjacent_intervals, And.intro
-- 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
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
apply : [[a, b₁]] ⊆ [[min a b₁, max a b₂]]
⊢ IntervalIntegrable f μ a b₁

Tactic:
apply h_int.mono_set

Premises used: IntervalIntegrable.mono_set
-- 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
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
h₃ : a ∈ [[min a b₁, max a b₂]]
h₄ : b₁ ∈ [[min a b₁, max a b₂]]
⊢ [[a, b₁]] ⊆ [[min a b₁, max a b₂]]

Tactic:
apply uIcc_subset_uIcc

Premises used: Set.uIcc_subset_uIcc
-- 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
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ a ∈ [[min a b₁, max a b₂]]

Tactic:
⟨min_le_of_left_le (min_le_left a b₁), le_max_of_le_right (le_max_left _ _)⟩

Premises used: Set.Mem, setOf, min_le_of_left_le, min_le_left, Set.Icc, le_max_of_le_right, And.intro, le_max_left, Set.uIcc
-- 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
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ a ∈ [[min a b₁, max a b₂]]

Tactic:
exact ⟨min_le_of_left_le (min_le_left a b₁), le_max_of_le_right (le_max_left _ _)⟩
-- 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
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ b₁ ∈ [[min a b₁, max a b₂]]

Tactic:
⟨min_le_of_left_le (min_le_right _ _),
          le_max_of_le_right (h₁.trans <| h₂.trans (le_max_right a b₂))⟩

Premises used: le_max_right, Set.Mem, setOf, min_le_of_left_le, Set.Icc, le_max_of_le_right, And.intro, min_le_right, LE.le.trans, Set.uIcc
-- 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
b : ℝ
h₁ : b₁ ≤ b
h₂ : b ≤ b₂
⊢ b₁ ∈ [[min a b₁, max a b₂]]

Tactic:
exact ⟨min_le_of_left_le (min_le_right _ _),
          le_max_of_le_right (h₁.trans <| h₂.trans (le_max_right a b₂))⟩
-- 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
⊢ ∀ b ∈ Icc b₁ b₂,
    ∫ (x : ℝ) in a..b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..b, f x ∂μ)

Tactic:
have : ∀ b ∈ Icc b₁ b₂,
        ∫ x in a..b, f x ∂μ = (∫ x in a..b₁, f x ∂μ) + ∫ x in b₁..b, f x ∂μ := by
      rintro b ⟨h₁, h₂⟩
      rw [← integral_add_adjacent_intervals _ (h_int' ⟨h₁, h₂⟩)]
      apply h_int.mono_set
      apply uIcc_subset_uIcc
      · exact ⟨min_le_of_left_le (min_le_left a b₁), le_max_of_le_right (le_max_left _ _)⟩
      · exact ⟨min_le_of_left_le (min_le_right _ _),
          le_max_of_le_right (h₁.trans <| h₂.trans (le_max_right a b₂))⟩
-- 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 :
  ∀ b ∈ Icc b₁ b₂,
    ∫ (x : ℝ) in a..b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..b, f x ∂μ)
apply :
  ContinuousWithinAt.{0, u_1} (Y := E)
    (fun (y : ℝ) ↦ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..y, f x ∂μ)) (Icc b₁ b₂) b₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
apply ContinuousWithinAt.congr _ this (this _ h₀)

Premises used: ContinuousWithinAt.congr
-- 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
⊢ ContinuousWithinAt.{0, u_1} (Y := E)
    (fun (y : ℝ) ↦ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..y, f x ∂μ)) (Icc b₁ b₂) b₀

Tactic:
continuousWithinAt_const.add ?_

Premises used: ContinuousWithinAt.add, 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
refine : ContinuousWithinAt.{0, u_1} (Y := E) (fun (y : ℝ) ↦ ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E)
    (fun (y : ℝ) ↦ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b₁, f x ∂μ) (∫ (x : ℝ) in b₁..y, f x ∂μ)) (Icc b₁ b₂) b₀

Tactic:
refine continuousWithinAt_const.add ?_

Premises used: ContinuousWithinAt.add, 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
apply :
  EqOn.{0, u_1} (β := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ)
    (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
⊢ 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 ∂μ

Tactic:
apply eventuallyEq_of_mem self_mem_nhdsWithin

Premises used: Filter.eventuallyEq_of_mem, self_mem_nhdsWithin
-- 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
⊢ EqOn.{0, u_1} (β := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ)
    (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)

Tactic:
fun b b_in => (integral_indicator b_in).symm

Premises used: Set.EqOn, intervalIntegral.integral_indicator, Eq.symm
-- 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
⊢ EqOn.{0, u_1} (β := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ)
    (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)

Tactic:
exact fun b b_in => (integral_indicator b_in).symm

Premises used: intervalIntegral.integral_indicator, Eq.symm
-- 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
⊢ 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 ∂μ

Tactic:
have :
      (fun b => ∫ x in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b =>
        ∫ x in b₁..b₂, indicator {x | x ≤ b} f x ∂μ := by
      apply eventuallyEq_of_mem self_mem_nhdsWithin
      exact fun b b_in => (integral_indicator b_in).symm
-- 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 :
  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 ∂μ
apply :
  ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
    b₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (y : ℝ) ↦ ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀

Tactic:
apply ContinuousWithinAt.congr_of_eventuallyEq _ this (integral_indicator h₀).symm

Premises used: ContinuousWithinAt.congr_of_eventuallyEq, intervalIntegral.integral_indicator, Eq.symm
-- 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 :
  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 ∂μ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖f x‖) μ b₁ b₂

Tactic:
have : IntervalIntegrable (fun x => ‖f x‖) μ b₁ b₂ :=
      IntervalIntegrable.norm (h_int' <| right_mem_Icc.mpr h₁₂)