awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n m : ℕ
hnm : n ≤ m
a : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((fun (n : ℕ) (a : α) ↦ (⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a : ℝ≥0∞)) m a)
    ((fun (n : ℕ) (a : α) ↦ (⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a : ℝ≥0∞)) n a)

Tactic:
iSup_le_iSup_of_subset fun i hi => le_trans hnm hi

Premises used: Set.Mem, iSup_le_iSup_of_subset, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n m : ℕ
hnm : n ≤ m
a : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0∞) a) ((fun (n : ℕ) (a : α) ↦ (⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a : ℝ≥0∞)) m a)
    ((fun (n : ℕ) (a : α) ↦ (⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a : ℝ≥0∞)) n a)

Tactic:
exact iSup_le_iSup_of_subset fun i hi => le_trans hnm hi

Premises used: iSup_le_iSup_of_subset, le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ∂μ ≠ ∞

Tactic:
ne_top_of_le_ne_top h_fin (lintegral_mono_ae ?_)

Premises used: MeasureTheory.lintegral_mono_ae, ne_top_of_le_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
refine_3 : ∀ᵐ (a : α) ∂μ, ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ≤ g a
⊢ ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ∂μ ≠ ∞

Tactic:
refine ne_top_of_le_ne_top h_fin (lintegral_mono_ae ?_)

Premises used: MeasureTheory.lintegral_mono_ae, ne_top_of_le_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ≤ g a

Tactic:
(ae_all_iff.2 h_bound).mono fun n hn => ?_

Premises used: Iff.mpr, Filter.Eventually.mono, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
refine_3 : ∀ (n : α) (hn : ∀ (i : ℕ), f i n ≤ g n), ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i n ≤ g n
⊢ ∀ᵐ (a : α) ∂μ, ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ≤ g a

Tactic:
refine (ae_all_iff.2 h_bound).mono fun n hn => ?_

Premises used: Iff.mpr, Filter.Eventually.mono, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n : α
hn : ∀ (i : ℕ), f i n ≤ g n
⊢ ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i n ≤ g n

Tactic:
iSup_le fun i => iSup_le fun _ => hn i

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
n : α
hn : ∀ (i : ℕ), f i n ≤ g n
⊢ ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i n ≤ g n

Tactic:
exact iSup_le fun i => iSup_le fun _ => hn i

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), limsup (fun (n : ℕ) ↦ f n a) atTop ∂μ

Tactic:
simp only [limsup_eq_iInf_iSup_of_nat]

Premises used: Filter.limsup_eq_iInf_iSup_of_nat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), Measurable (F n)
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), F n a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
tendsto_of_le_liminf_of_limsup_le
    (calc
      ∫⁻ a, f a ∂μ = ∫⁻ a, liminf (fun n : ℕ => F n a) atTop ∂μ :=
        lintegral_congr_ae <| h_lim.mono fun _ h => h.liminf_eq.symm
      _ ≤ liminf (fun n => ∫⁻ a, F n a ∂μ) atTop := lintegral_liminf_le hF_meas)
    (calc
      limsup (fun n : ℕ => ∫⁻ a, F n a ∂μ) atTop ≤ ∫⁻ a, limsup (fun n => F n a) atTop ∂μ :=
        limsup_lintegral_le _ hF_meas h_bound h_fin
      _ = ∫⁻ a, f a ∂μ := lintegral_congr_ae <| h_lim.mono fun _ h => h.limsup_eq)

Premises used: Filter.Tendsto.limsup_eq, Trans.trans, MeasureTheory.limsup_lintegral_le, MeasureTheory.lintegral_liminf_le, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono, Filter.Tendsto.liminf_eq, tendsto_of_le_liminf_of_limsup_le, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ

Tactic:
have : ∀ n, ∫⁻ a, F n a ∂μ = ∫⁻ a, (hF_meas n).mk (F n) a ∂μ := fun n =>
    lintegral_congr_ae (hF_meas n).ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
simp_rw : Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), F n a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
simp_rw [this]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
tendsto_lintegral_of_dominated_convergence :
  ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))
tendsto_lintegral_of_dominated_convergence₁ : ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ ≤ᶠ[ae μ] bound
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
apply
    tendsto_lintegral_of_dominated_convergence bound (fun n => (hF_meas n).measurable_mk) _ h_fin

Premises used: MeasureTheory.tendsto_lintegral_of_dominated_convergence, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a

Tactic:
have : ∀ n, ∀ᵐ a ∂μ, (hF_meas n).mk (F n) a = F n a := fun n => (hF_meas n).ae_eq_mk.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this_1 : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
⊢ ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a

Tactic:
have : ∀ᵐ a ∂μ, ∀ n, (hF_meas n).mk (F n) a = F n a := ae_all_iff.mpr this
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this_1 : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this_2 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
this : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
h :
  ∀ (a : α) (H : ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a) (H' : Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))),
    Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

Tactic:
filter_upwards [this, h_lim] with a H H'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this_1 : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this_2 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
this : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
a : α
H : ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
H' h : Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))

Tactic:
simp_rw [H]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this_1 : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this_2 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
this : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
a : α
H : ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
H' : Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))

Tactic:
H'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this_1 : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this_2 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
this : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
a : α
H : ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
H' : Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))

Tactic:
exact H'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
n : ℕ
h : ∀ (a : α) (H : F n a ≤ bound a) (H' : F n a = AEMeasurable.mk (F n) ⋯ a), AEMeasurable.mk (F n) ⋯ a ≤ bound a
⊢ AEMeasurable.mk (F n) ⋯ ≤ᶠ[ae μ] bound

Tactic:
filter_upwards [h_bound n, (hF_meas n).ae_eq_mk] with a H H'

Premises used: AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
n : ℕ
a : α
H : F n a ≤ bound a
H' : F n a = AEMeasurable.mk (F n) ⋯ a
h h₁ h₂ h₃ :
  ∀ (H : AEMeasurable.mk (F n) ⋯ a ≤ bound a) (H' : F n a = AEMeasurable.mk (F n) ⋯ a),
    AEMeasurable.mk (F n) ⋯ a ≤ bound a
⊢ AEMeasurable.mk (F n) ⋯ a ≤ bound a

Tactic:
rwa [H'] at H
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
rw :
  ∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
⊢ Tendsto (fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
rw [tendsto_iff_seq_tendsto]

Premises used: Filter.tendsto_iff_seq_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s

Tactic:
rw [tendsto_atTop'] at xl

Premises used: Filter.tendsto_atTop'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl_1 : Tendsto x atTop l
xl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
⊢ ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s

Tactic:
xl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl_1 : Tendsto x atTop l
xl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
⊢ ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s

Tactic:
exact xl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s

Tactic:
have hxl := by
    rw [tendsto_atTop'] at xl
    exact xl
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
⊢ {x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x} ∈ l

Tactic:
have h := inter_mem hF_meas h_bound
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h : {x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x} ∈ l
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      Membership.mem (γ := Set ι)
        ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
        (x b)

Tactic:
replace h := hxl _ h
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h :
  ∃ (a : ℕ),
    ∀ b ≥ a,
      Membership.mem (γ := Set ι)
        ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
        (x b)
rcases :
  ∀ (k : ℕ)
    (h :
      ∀ b ≥ k,
        Membership.mem (γ := Set ι)
          ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩
            {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
          (x b)),
    Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
⊢ Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
rcases h with ⟨k, h⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
rw : Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
⊢ Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
rw [← tendsto_add_atTop_iff_nat k]

Premises used: Filter.tendsto_add_atTop_iff_nat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
tendsto_lintegral_of_dominated_convergence' ?_ ?_ ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_lintegral_of_dominated_convergence'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
refine_1 : α → ℝ≥0∞
refine_2 : ∀ (n : ℕ), AEMeasurable (F (x (n + k))) μ
refine_3 : ∀ (n : ℕ), F (x (n + k)) ≤ᶠ[ae μ] bound
refine_4 : ∫⁻ (a : α), bound a ∂μ ≠ ∞
refine_5 : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F (x (n + k)) a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
refine tendsto_lintegral_of_dominated_convergence' ?_ ?_ ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_lintegral_of_dominated_convergence'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
⊢ α → ℝ≥0∞

Tactic:
exact bound
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
n : ℕ
⊢ AEMeasurable (F (x (n + k))) μ

Tactic:
(h _ ?_).1

Premises used: AEMeasurable, Set.Mem, setOf, And.left