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 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖f x‖) μ b₁ b₂
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
    b₀

Tactic:
continuousWithinAt_of_dominated_interval ?_ ?_ this ?_

Premises used: intervalIntegral.continuousWithinAt_of_dominated_interval
-- 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 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖f x‖) μ b₁ b₂
refine_1 : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))
refine_2 : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
refine_3 :
  ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι b₁ b₂ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f t) (Icc b₁ b₂) b₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
    b₀

Tactic:
refine continuousWithinAt_of_dominated_interval ?_ ?_ this ?_

Premises used: intervalIntegral.continuousWithinAt_of_dominated_interval
-- 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 ∂μ
h : ∀ a ∈ Icc b₁ b₂, AEStronglyMeasurable (indicator {x : ℝ | x ≤ a} f) (μ.restrict (Ι b₁ b₂))
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))

Tactic:
filter_upwards [self_mem_nhdsWithin]

Premises used: 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
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 ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
h : AEStronglyMeasurable f (μ.restrict (Ioc (min b₁ b₂) x))
h₁ : x ≤ max b₁ b₂
h₂ h₃ : MeasurableSet (α := ℝ) {x_1 : ℝ | x_1 ≤ x}
⊢ AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))

Tactic:
rw [aestronglyMeasurable_indicator_iff, Measure.restrict_restrict, uIoc, Iic_def,
        Iic_inter_Ioc_of_le]

Premises used: Set.uIoc, MeasureTheory.Measure.restrict_restrict, Set.Iic_inter_Ioc_of_le, Set.Iic_def, aestronglyMeasurable_indicator_iff
-- 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 ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
h : AEStronglyMeasurable f (μ.restrict (Ioc b₁ x))
⊢ AEStronglyMeasurable f (μ.restrict (Ioc (min b₁ b₂) x))

Tactic:
rw [min₁₂]
-- 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 ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ AEStronglyMeasurable f (μ.restrict (Ioc b₁ x))

Tactic:
(h_int' hx).1.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, And.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
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 ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ AEStronglyMeasurable f (μ.restrict (Ioc b₁ x))

Tactic:
exact (h_int' hx).1.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, And.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
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 ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ x ≤ max b₁ b₂

Tactic:
le_max_of_le_right hx.2

Premises used: And.right, le_max_of_le_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
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 ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ x ≤ max b₁ b₂

Tactic:
exact le_max_of_le_right hx.2

Premises used: And.right, le_max_of_le_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
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 ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ MeasurableSet (α := ℝ) {x_1 : ℝ | x_1 ≤ x}

Tactic:
measurableSet_Iic

Premises used: setOf, measurableSet_Iic, Set.Iic
-- 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 ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ MeasurableSet (α := ℝ) {x_1 : ℝ | x_1 ≤ x}

Tactic:
exacts [measurableSet_Iic, measurableSet_Iic]

Premises used: measurableSet_Iic
-- 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 ∂μ
refine_2 : ∀ (x : ℝ), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖

Tactic:
filter_upwards with x
-- 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 ∂μ
x : ℝ
refine_2 : ∀ t ∈ Ι b₁ b₂, ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖

Tactic:
filter_upwards with t
-- 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 ∂μ
x t : ℝ
refine_2 : t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖
⊢ t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖

Tactic:
dsimp [indicator]

Premises used: Set.indicator
-- 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 ∂μ
x t : ℝ
pos : t ≤ x → t ∈ Ι b₁ b₂ → ‖f t‖ ≤ ‖f t‖
neg : ¬t ≤ x → t ∈ Ι b₁ b₂ → norm.{u_1} (E := E) 0 ≤ ‖f t‖
⊢ t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖

Tactic:
split_ifs
-- 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 ∂μ
x t : ℝ
h : t ≤ x
⊢ t ∈ Ι b₁ b₂ → ‖f t‖ ≤ ‖f t‖

Tactic:
simp
-- 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 ∂μ
x t : ℝ
h : ¬t ≤ x
⊢ t ∈ Ι b₁ b₂ → norm.{u_1} (E := E) 0 ≤ ‖f t‖

Tactic:
simp
-- 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 ∂μ
x : ℝ
hx : Membership.mem (γ := Set ℝ) {b₀}ᶜ x
⊢ x < b₀ ∨ b₀ < x

Tactic:
Ne.lt_or_gt hx

Premises used: Ne.lt_or_gt
-- 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 ∂μ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {b₀}ᶜ x → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (t : ℝ) ↦ t < b₀ ∨ b₀ < t) x} x}
      a
h₁ h₂ : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) {b₀}ᶜ x), x < b₀ ∨ b₀ < x
⊢ ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t

Tactic:
filter_upwards [compl_mem_ae_iff.mpr hb₀] with x hx using Ne.lt_or_gt hx

Premises used: Iff.mpr, MeasureTheory.compl_mem_ae_iff
-- 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 ∂μ
⊢ ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t

Tactic:
have : ∀ᵐ t ∂μ, t < b₀ ∨ b₀ < t := by
        filter_upwards [compl_mem_ae_iff.mpr hb₀] with x hx using Ne.lt_or_gt 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
refine_3 :
  ∀ (x : ℝ),
    x < b₀ ∨ b₀ < x →
      x ∈ Ι b₁ b₂ →
        ContinuousWithinAt.{0, u_1} (Y := E) (fun (x_1 : ℝ) ↦ indicator {x : ℝ | x ≤ x_1} f x) (Icc b₁ b₂) b₀
⊢ ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι b₁ b₂ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f t) (Icc b₁ b₂) b₀

Tactic:
apply this.mono

Premises used: 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₀ : x₀ < b₀
h : {x : ℝ | (fun (x : ℝ) ↦ indicator {t : ℝ | t ≤ x} f x₀ = f x₀) x} ∈ 𝓝 b₀
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = f x₀

Tactic:
apply mem_nhdsWithin_of_mem_nhds

Premises used: mem_nhdsWithin_of_mem_nhds
-- 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₀ : x₀ < b₀
h : ∀ (x : ℝ), x₀ < x → indicator {t : ℝ | t ≤ x} f x₀ = f x₀
⊢ {x : ℝ | (fun (x : ℝ) ↦ indicator {t : ℝ | t ≤ x} f x₀ = f x₀) x} ∈ 𝓝 b₀

Tactic:
apply Eventually.mono (Ioi_mem_nhds hx₀)

Premises used: Ioi_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₀ : x₀ < b₀
x : ℝ
hx : x₀ < x
⊢ indicator {t : ℝ | t ≤ x} f x₀ = f x₀

Tactic:
simp [hx.le]

Premises used: LT.lt.le
-- 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₀ : x₀ < b₀
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = f x₀

Tactic:
have : ∀ᶠ x in 𝓝[Icc b₁ b₂] b₀, {t : ℝ | t ≤ x}.indicator f x₀ = f x₀ := by
          apply mem_nhdsWithin_of_mem_nhds
          apply Eventually.mono (Ioi_mem_nhds hx₀)
          intro x hx
          simp [hx.le]
-- 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₀ : x₀ < b₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = f x₀
refine_3 : indicator {t : ℝ | t ≤ b₀} f x₀ = f x₀
⊢ 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₀ : x₀ < b₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = f x₀
⊢ indicator {t : ℝ | t ≤ b₀} f x₀ = f x₀

Tactic:
simp [hx₀.le]

Premises used: LT.lt.le
-- 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 : ℝ | (fun (x : ℝ) ↦ indicator {t : ℝ | t ≤ x} f x₀ = 0) x} ∈ 𝓝 b₀
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = 0

Tactic:
apply mem_nhdsWithin_of_mem_nhds

Premises used: mem_nhdsWithin_of_mem_nhds