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
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = enorm (E := ℝ) (∫ (a : α), ‖F i a‖ ∂μ)

Tactic:
have (i : ι) : ∫⁻ a, ‖F i a‖ₑ ∂μ = ‖∫ a, ‖F i a‖ ∂μ‖ₑ := by
    dsimp [enorm]
    rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
      Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]
    simp only [coe_nnnorm]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = enorm (E := ℝ) (∫ (a : α), ‖F i a‖ ∂μ)
pos : Ne (α := ℝ≥0∞) (∑' (x : ι), enorm (E := ℝ) (∫ (a : α), ‖F x a‖ ∂μ)) ∞
⊢ Ne (α := ℝ≥0∞) (∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ) ∞

Tactic:
rw [funext this]

Premises used: funext
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = enorm (E := ℝ) (∫ (a : α), ‖F i a‖ ∂μ)
⊢ Ne (α := ℝ≥0∞) (∑' (x : ι), enorm (E := ℝ) (∫ (a : α), ‖F x a‖ ∂μ)) ∞

Tactic:
ENNReal.tsum_coe_ne_top_iff_summable.2 <| NNReal.summable_coe.1 hF_sum.abs

Premises used: NNReal.summable_coe, Iff.mpr, Summable.abs, ENNReal.tsum_coe_ne_top_iff_summable, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
this : ∀ (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ = enorm (E := ℝ) (∫ (a : α), ‖F i a‖ ∂μ)
⊢ Ne (α := ℝ≥0∞) (∑' (x : ι), enorm (E := ℝ) (∫ (a : α), ‖F x a‖ ∂μ)) ∞

Tactic:
exact ENNReal.tsum_coe_ne_top_iff_summable.2 <| NNReal.summable_coe.1 hF_sum.abs

Premises used: NNReal.summable_coe, Iff.mpr, ENNReal.tsum_coe_ne_top_iff_summable, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst_2 : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable (α := ℝ) fun (i : ι) ↦ ∫ (a : α), ‖F i a‖ ∂μ
⊢ Eq.{u_2 + 1} (α := E) (∑' (i : ι), ∫ (a : α), F i a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
(hasSum_integral_of_summable_integral_norm hF_int hF_sum).tsum_eq

Premises used: HasSum.tsum_eq, MeasureTheory.hasSum_integral_of_summable_integral_norm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → α → G
inst_3 : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∃ (C : ℝ), ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ C
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (n : ι) ↦ F n ω) l (𝓝 (f ω))
obtain :
  ∀ (c : ℝ) (h_boundc : ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ c),
    Tendsto.{u_4, u_3} (β := G) (fun (n : ι) ↦ ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))
⊢ Tendsto.{u_4, u_3} (β := G) (fun (n : ι) ↦ ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Tactic:
obtain ⟨c, h_boundc⟩ := h_bound
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → α → G
inst_3 : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (n : ι) ↦ F n ω) l (𝓝 (f ω))
c : ℝ
h_boundc : ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ c
C : α → ℝ := fun (x : α) ↦ c
⊢ Tendsto.{u_4, u_3} (β := G) (fun (n : ι) ↦ ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Tactic:
tendsto_integral_filter_of_dominated_convergence
    C h_meas h_boundc (integrable_const c) h_lim

Premises used: MeasureTheory.tendsto_integral_filter_of_dominated_convergence, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
G : Type u_3
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → α → G
inst_3 : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (n : ι) ↦ F n ω) l (𝓝 (f ω))
c : ℝ
h_boundc : ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ c
C : α → ℝ := fun (x : α) ↦ c
⊢ Tendsto.{u_4, u_3} (β := G) (fun (n : ι) ↦ ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Tactic:
exact tendsto_integral_filter_of_dominated_convergence
    C h_meas h_boundc (integrable_const c) h_lim

Premises used: MeasureTheory.tendsto_integral_filter_of_dominated_convergence, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
⊢ Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ

Tactic:
have h_int_eq : (fun i => ∫ a in s i, f a ∂μ) = fun i => ∫ a, (s i).indicator f a ∂μ :=
    funext fun i => (integral_indicator (hsm i)).symm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
rw :
  Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) atTop (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))

Tactic:
rw [h_int_eq]
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
rw :
  Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) f x ∂μ))
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (a : α) in ⋂ (n : ℕ), s n, f a ∂μ))

Tactic:
rw [← integral_indicator (MeasurableSet.iInter hsm)]

Premises used: MeasureTheory.integral_indicator, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) f x ∂μ))

Tactic:
tendsto_integral_of_dominated_convergence bound ?_ ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_integral_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_1 : ∀ (n : ℕ), AEStronglyMeasurable ((s n).indicator f) μ
refine_2 : Integrable bound μ
refine_3 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖(s n).indicator f a‖ ≤ bound a
refine_4 : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))
⊢ Tendsto.{0, u_2} (β := E) (fun (i : ℕ) ↦ ∫ (a : α), (s i).indicator f a ∂μ) atTop
    (𝓝 (∫ (x : α), indicator (⋂ (b : ℕ), s b) f x ∂μ))

Tactic:
refine tendsto_integral_of_dominated_convergence bound ?_ ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_integral_of_dominated_convergence
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
refine_1 : AEStronglyMeasurable f (μ.restrict (s n))
⊢ AEStronglyMeasurable ((s n).indicator f) μ

Tactic:
rw [aestronglyMeasurable_indicator_iff (hsm n)]

Premises used: aestronglyMeasurable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable f (μ.restrict (s n))

Tactic:
(IntegrableOn.mono_set hfi (h_anti zero_le)).1

Premises used: zero_le, MeasureTheory.IntegrableOn.mono_set, And.left
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
⊢ AEStronglyMeasurable f (μ.restrict (s n))

Tactic:
exact (IntegrableOn.mono_set hfi (h_anti zero_le)).1

Premises used: zero_le, MeasureTheory.IntegrableOn.mono_set, And.left
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_2 : IntegrableOn (ε := ℝ) (fun (a : α) ↦ ‖f a‖) (s 0) μ
⊢ Integrable bound μ

Tactic:
rw [integrable_indicator_iff (hsm 0)]

Premises used: OfNat.ofNat, MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ IntegrableOn (ε := ℝ) (fun (a : α) ↦ ‖f a‖) (s 0) μ

Tactic:
hfi.norm

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ IntegrableOn (ε := ℝ) (fun (a : α) ↦ ‖f a‖) (s 0) μ

Tactic:
exact hfi.norm

Premises used: MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_3 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, (s n).indicator (fun (a : α) ↦ ‖f a‖) a ≤ bound a
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖(s n).indicator f a‖ ≤ bound a

Tactic:
simp_rw [norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, (s n).indicator (fun (a : α) ↦ ‖f a‖) a ≤ bound a

Tactic:
fun n => Eventually.of_forall fun x => ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_3 : ∀ (n : ℕ) (x : α), (s n).indicator (fun (a : α) ↦ ‖f a‖) x ≤ bound x
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, (s n).indicator (fun (a : α) ↦ ‖f a‖) a ≤ bound a

Tactic:
refine fun n => Eventually.of_forall fun x => ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
x : α
h₁ : 0 ≤ ‖f x‖
refine_3 refine_3₁ : LE.le (α := ℝ) ((s 0).indicator (fun (a : α) ↦ ‖f a‖) x) ((s 0).indicator (fun (a : α) ↦ ‖f a‖) x)
⊢ (s n).indicator (fun (a : α) ↦ ‖f a‖) x ≤ bound x

Tactic:
grw [(h_anti zero_le).subset]

Premises used: zero_le, LE.le.subset
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
a : α
⊢ Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))

Tactic:
le_trans (h_anti.tendsto_indicator _ _ _) (pure_le_nhds _)

Premises used: pure_le_nhds, Antitone.tendsto_indicator, Filter.Tendsto, le_trans
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
α : Type u_1
E : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun (a : α) ↦ ‖f a‖
h_int_eq :
  Eq.{u_2 + 1} (α := (i : ℕ) → E) (fun (i : ℕ) ↦ ∫ (a : α) in s i, f a ∂μ) fun (i : ℕ) ↦
    ∫ (a : α), (s i).indicator f a ∂μ
refine_4 :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α | (fun (a : α) ↦ Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))) x}
      a
refine_4₁ refine_4₂ : ∀ (a : α), Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ (s n).indicator f a) atTop (𝓝 (indicator (⋂ (b : ℕ), s b) f a))

Tactic:
filter_upwards [] with a using le_trans (h_anti.tendsto_indicator _ _ _) (pure_le_nhds _)

Premises used: pure_le_nhds, Antitone.tendsto_indicator, le_trans
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))
simp :
  ∀ (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound x)
    (bound_integrable : IntegrableOn bound (Ι a b) μ)
    (h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))),
    Tendsto (fun (n : ι) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, F n x ∂μ)) l
      (𝓝 (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ)))
⊢ Tendsto.{u_3, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc,
    ← ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *

Premises used: intervalIntegrable_iff, intervalIntegral.intervalIntegral_eq_integral_uIoc, measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound x
bound_integrable : IntegrableOn bound (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))
⊢ Tendsto (fun (n : ι) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, F n x ∂μ)) l
    (𝓝 (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ)))

Tactic:
tendsto_const_nhds.smul <|
    tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_lim

Premises used: tendsto_const_nhds, MeasureTheory.tendsto_integral_filter_of_dominated_convergence, Filter.Tendsto.smul
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound x
bound_integrable : IntegrableOn bound (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Tendsto (fun (n : ι) ↦ F n x) l (𝓝 (f x))
⊢ Tendsto (fun (n : ι) ↦ HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, F n x ∂μ)) l
    (𝓝 (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ)))

Tactic:
exact tendsto_const_nhds.smul <|
    tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_lim

Premises used: tendsto_const_nhds, Filter.Tendsto.smul
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
inl :
  ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥] (hF : ∀ᶠ (i : ι) in ⊥, ContinuousOn (F i) [[a, b]])
    (h_lim : TendstoUniformlyOn F f ⊥ [[a, b]]),
    Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) ⊥ (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
inr :
  ∀ (hl : l.NeBot),
    Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
rcases l.eq_or_neBot with rfl | hl

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
F : ι → ℝ → E
inst_2 : IsLocallyFiniteMeasure μ
inst_3 : IsCountablyGenerated.{u_1} (α := ι) ⊥
hF : ∀ᶠ (i : ι) in ⊥, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f ⊥ [[a, b]]
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) ⊥ (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
l : Filter ι
inst_2 : l.IsCountablyGenerated
F : ι → ℝ → E
inst_3 : IsLocallyFiniteMeasure μ
hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) [[a, b]]
h_lim : TendstoUniformlyOn F f l [[a, b]]
hl : l.NeBot
inr :
  ∀ (C : ℝ) (hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : ℝ) ↦ ‖f x‖) '' [[a, b]])) C),
    Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
⊢ Tendsto.{u_1, u_2} (β := E) (fun (n : ι) ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
rcases isCompact_uIcc.bddAbove_image (h_lim.continuousOn hF.frequently).norm with ⟨C, hC⟩

Premises used: isCompact_uIcc, IsCompact.bddAbove_image, Filter.Eventually.frequently, ContinuousOn.norm, TendstoUniformlyOn.continuousOn