awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
h : (Ioi a).indicator (fun (a : ℝ) ↦ ‖f a‖) x ≤ (Ioi a₀).indicator (norm ∘ f) x
⊢ ‖(Ioi a).indicator f x‖ ≤ (Ioi a₀).indicator (norm ∘ f) x

Tactic:
rw [norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
⊢ a₀ ≤ a

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
⊢ (Ioi a).indicator (fun (a : ℝ) ↦ ‖f a‖) x ≤ (Ioi a₀).indicator (norm ∘ f) x

Tactic:
apply indicator_le_indicator_of_subset (Ioi_subset_Ioi (by grind)) (fun a ↦ norm_nonneg (f a))

Premises used: Set.indicator_le_indicator_of_subset, Set.Ioi_subset_Ioi
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ Integrable ((Ioi a₀).indicator (norm ∘ f)) μ

Tactic:
simpa [integrable_indicator_iff measurableSet_Ioi] using hf.norm

Premises used: measurableSet_Ioi, MeasureTheory.Integrable.norm, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))

Tactic:
ae_of_all _ fun x ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
h_lim : ∀ (x : ℝ), Tendsto (fun (n : ℝ) ↦ (Ioi n).indicator f x) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f x))
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))

Tactic:
refine ae_of_all _ fun x ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
pos : ∀ (hx : a₀ < x), Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
neg : ∀ (hx : ¬a₀ < x), Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
⊢ Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))

Tactic:
by_cases hx : a₀ < x
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
pos :
  EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
    if n < x then f x else 0
⊢ Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
neg :
  EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
    if n < x then f x else 0
⊢ Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
a : ℝ
ha : a ∈ Iio x
⊢ (if a₀ < x then f x else 0) = if a < x then f x else 0

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Iio x →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ |
              (fun (x_3 : ℝ) ↦
                  Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if a₀ < x then f x else 0) x_3)
                    ((fun (n : ℝ) ↦ if n < x then f x else 0) x_3))
                x_2}
            x_1}
      a
h₁ h₂ : ∀ (a : ℝ) (ha : a ∈ Iio x), (if a₀ < x then f x else 0) = if a < x then f x else 0
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
    if n < x then f x else 0

Tactic:
filter_upwards [mem_nhdsWithin_of_mem_nhds (Iio_mem_nhds hx)] with a ha using by grind

Premises used: Iio_mem_nhds, mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
a : ℝ
ha : a ∈ Ici a₀
⊢ (if a₀ < x then f x else 0) = if a < x then f x else 0

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Ici a₀ →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ |
              (fun (x_3 : ℝ) ↦
                  Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if a₀ < x then f x else 0) x_3)
                    ((fun (n : ℝ) ↦ if n < x then f x else 0) x_3))
                x_2}
            x_1}
      a
h₁ h₂ : ∀ (a : ℝ) (ha : a ∈ Ici a₀), (if a₀ < x then f x else 0) = if a < x then f x else 0
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
    if n < x then f x else 0

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha using by grind

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
a₁ : ∀ (ha : a₀ ≤ a), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a
⊢ a ∈ Ici a₀ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a

Tactic:
(ha : a₀ ≤ a)
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
rw :
  ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Iic a) a ∧
    ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a

Tactic:
rw [continuousWithinAt_iff_continuous_left_right]

Premises used: continuousWithinAt_iff_continuous_left_right
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
left : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Iic a) a
right : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Iic a) a ∧
    ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
⊢ IntervalIntegrable f μ a₀ a

Tactic:
have h_int : IntervalIntegrable f μ a₀ a :=
      (intervalIntegrable_iff_integrableOn_Ioc_of_le ha).2 <| hf.mono_set Ioc_subset_Ioi_self
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
b : ℝ
hb : b ∈ Icc a₀ a
⊢ ∫ (x : ℝ) in Ioi b, f x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)

Tactic:
simp [← integral_Ioi_sub_Ioi hf hb.1]

Premises used: intervalIntegral.integral_Ioi_sub_Ioi, And.left
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
⊢ ∀ b ∈ Icc a₀ a,
    ∫ (x : ℝ) in Ioi b, f x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)

Tactic:
have h_split : ∀ b ∈ Icc a₀ a, ∫ x in Ioi b, f x ∂μ =
        (∫ x in Ioi a₀, f x ∂μ) - ∫ x in a₀..b, f x ∂μ := by
      intro b hb
      simp [← integral_Ioi_sub_Ioi hf hb.1]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
h_split :
  ∀ b ∈ Icc a₀ a,
    ∫ (x : ℝ) in Ioi b, f x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)
⊢ IntervalIntegrable f μ (min a₀ a₀) (max a₀ a)

Tactic:
simpa [ha]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
h_split :
  ∀ b ∈ Icc a₀ a,
    ∫ (x : ℝ) in Ioi b, f x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a₀..b, f x ∂μ) (Icc a₀ a) a

Tactic:
have h_cwa : ContinuousWithinAt (fun b ↦ ∫ x in a₀..b, f x ∂μ) (Icc a₀ a) a :=
      continuousWithinAt_primitive (measure_singleton a) (by simpa [ha])
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
h_split :
  ∀ b ∈ Icc a₀ a,
    ∫ (x : ℝ) in Ioi b, f x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)
h_cwa : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a₀..b, f x ∂μ) (Icc a₀ a) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Icc a₀ a) a

Tactic:
(continuousWithinAt_const.sub h_cwa).congr h_split (h_split a (right_mem_Icc.2 ha))

Premises used: Iff.mpr, Set.right_mem_Icc, ContinuousWithinAt.sub, continuousWithinAt_const, ContinuousWithinAt.congr
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
h_split :
  ∀ b ∈ Icc a₀ a,
    ∫ (x : ℝ) in Ioi b, f x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)
h_cwa : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a₀..b, f x ∂μ) (Icc a₀ a) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Icc a₀ a) a

Tactic:
exact (continuousWithinAt_const.sub h_cwa).congr h_split (h_split a (right_mem_Icc.2 ha))

Premises used: Iff.mpr, Set.right_mem_Icc, ContinuousWithinAt.sub, continuousWithinAt_const, ContinuousWithinAt.congr
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a

Tactic:
simpa [ha] using (hf.mono_set (Ioi_subset_Ioi ha)).continuousWithinAt_Ici_primitive_Ioi

Premises used: MeasureTheory.IntegrableOn.continuousWithinAt_Ici_primitive_Ioi, MeasureTheory.IntegrableOn.mono_set, Set.Ioi_subset_Ioi
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
simp_rw : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Iio b).indicator f x ∂μ) (Iic a₀) a₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a₀

Tactic:
simp_rw [← integral_indicator measurableSet_Iio]

Premises used: MeasureTheory.integral_indicator, measurableSet_Iio
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, AEStronglyMeasurable ((Iio n).indicator f) μ
h_bound : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Iio n).indicator f a‖ ≤ (Iio a₀).indicator (norm ∘ f) a
bound_integrable : Integrable ((Iio a₀).indicator (norm ∘ f)) μ
h_lim : ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Iio n).indicator f a) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f a))
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Iio b).indicator f x ∂μ) (Iic a₀) a₀

Tactic:
apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f))

Premises used: Norm.norm, Set.indicator, MeasureTheory.tendsto_integral_filter_of_dominated_convergence, Function.comp, Set.Iio
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
h : ∀ (a : ℝ) (ha : a ∈ Iic a₀), AEStronglyMeasurable ((Iio a).indicator f) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, AEStronglyMeasurable ((Iio n).indicator f) μ

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
h : AEStronglyMeasurable f (μ.restrict (Iio a))
⊢ AEStronglyMeasurable ((Iio a).indicator f) μ

Tactic:
rw [aestronglyMeasurable_indicator_iff measurableSet_Iio]

Premises used: measurableSet_Iio, aestronglyMeasurable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ AEStronglyMeasurable f (μ.restrict (Iio a))

Tactic:
(hf.mono_set (Iio_subset_Iio ha)).aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Set.Iio_subset_Iio, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ AEStronglyMeasurable f (μ.restrict (Iio a))

Tactic:
exact (hf.mono_set (Iio_subset_Iio ha)).aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Set.Iio_subset_Iio, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
h : ∀ (a : ℝ) (ha : a ∈ Iic a₀), ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Iio a).indicator f a_1‖ ≤ (Iio a₀).indicator (norm ∘ f) a_1
⊢ ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Iio n).indicator f a‖ ≤ (Iio a₀).indicator (norm ∘ f) a

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Iio a).indicator f a_1‖ ≤ (Iio a₀).indicator (norm ∘ f) a_1

Tactic:
ae_of_all _ fun x ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
h : ∀ (x : ℝ), ‖(Iio a).indicator f x‖ ≤ (Iio a₀).indicator (norm ∘ f) x
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Iio a).indicator f a_1‖ ≤ (Iio a₀).indicator (norm ∘ f) a_1

Tactic:
refine ae_of_all _ fun x ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
x : ℝ
h : (Iio a).indicator (fun (a : ℝ) ↦ ‖f a‖) x ≤ (Iio a₀).indicator (norm ∘ f) x
⊢ ‖(Iio a).indicator f x‖ ≤ (Iio a₀).indicator (norm ∘ f) x

Tactic:
rw [norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
x : ℝ
⊢ a ≤ a₀

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
x : ℝ
⊢ (Iio a).indicator (fun (a : ℝ) ↦ ‖f a‖) x ≤ (Iio a₀).indicator (norm ∘ f) x

Tactic:
apply indicator_le_indicator_of_subset (Iio_subset_Iio (by grind)) (fun a ↦ norm_nonneg (f a))

Premises used: Set.indicator_le_indicator_of_subset, Set.Iio_subset_Iio
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ Integrable ((Iio a₀).indicator (norm ∘ f)) μ

Tactic:
simpa [integrable_indicator_iff measurableSet_Iio] using hf.norm

Premises used: measurableSet_Iio, MeasureTheory.Integrable.norm, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Iio n).indicator f a) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f a))

Tactic:
ae_of_all _ fun x ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
h_lim : ∀ (x : ℝ), Tendsto (fun (n : ℝ) ↦ (Iio n).indicator f x) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f x))
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Iio n).indicator f a) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f a))

Tactic:
refine ae_of_all _ fun x ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
pos : ∀ (hx : x < a₀), Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
neg : ∀ (hx : ¬x < a₀), Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))
⊢ Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))

Tactic:
by_cases hx : x < a₀
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : x < a₀
pos :
  EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
    if x < n then f x else 0
⊢ Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
neg :
  EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
    if x < n then f x else 0
⊢ Tendsto (fun (n : ℝ) ↦ if x < n then f x else 0) (𝓝[≤] a₀) (𝓝 (if x < a₀ then f x else 0))

Tactic:
apply tendsto_const_nhds.congr'

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : x < a₀
a : ℝ
ha : a ∈ Ioi x
⊢ (if x < a₀ then f x else 0) = if x < a then f x else 0

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : x < a₀
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Ioi x →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ |
              (fun (x_3 : ℝ) ↦
                  Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if x < a₀ then f x else 0) x_3)
                    ((fun (n : ℝ) ↦ if x < n then f x else 0) x_3))
                x_2}
            x_1}
      a
h₁ h₂ : ∀ (a : ℝ) (ha : a ∈ Ioi x), (if x < a₀ then f x else 0) = if x < a then f x else 0
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
    if x < n then f x else 0

Tactic:
filter_upwards [mem_nhdsWithin_of_mem_nhds (Ioi_mem_nhds hx)] with a ha using by grind

Premises used: Ioi_mem_nhds, mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
a : ℝ
ha : a ∈ Iic a₀
⊢ (if x < a₀ then f x else 0) = if x < a then f x else 0

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
x : ℝ
hx : ¬x < a₀
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Iic a₀ →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ |
              (fun (x_3 : ℝ) ↦
                  Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if x < a₀ then f x else 0) x_3)
                    ((fun (n : ℝ) ↦ if x < n then f x else 0) x_3))
                x_2}
            x_1}
      a
h₁ h₂ : ∀ (a : ℝ) (ha : a ∈ Iic a₀), (if x < a₀ then f x else 0) = if x < a then f x else 0
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≤] a₀) (fun (x_1 : ℝ) ↦ if x < a₀ then f x else 0) fun (n : ℝ) ↦
    if x < n then f x else 0

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha using by grind

Premises used: self_mem_nhdsWithin