awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
refine_2 : n + k ≥ k
⊢ AEMeasurable (F (x (n + k))) μ

Tactic:
refine (h _ ?_).1

Premises used: And.left
-- 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 : ℕ
⊢ n + k ≥ k

Tactic:
Nat.le_add_left _ _

Premises used: Nat.le_add_left
-- 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 : ℕ
⊢ n + k ≥ k

Tactic:
exact Nat.le_add_left _ _

Premises used: Nat.le_add_left
-- 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 : ℕ
⊢ F (x (n + k)) ≤ᶠ[ae μ] bound

Tactic:
(h _ ?_).2

Premises used: Set.Mem, Filter.Eventually, setOf, And.right, Filter.EventuallyLE
-- 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 : ℕ
refine_3 : n + k ≥ k
⊢ F (x (n + k)) ≤ᶠ[ae μ] bound

Tactic:
refine (h _ ?_).2

Premises used: And.right
-- 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)
⊢ ∫⁻ (a : α), bound a ∂μ ≠ ∞

Tactic:
assumption
-- 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)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
h_lim.mono fun a h_lim => ?_

Premises used: Filter.Eventually.mono
-- 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_5 :
  ∀ (a : α) (h_lim : Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))), Tendsto (fun (n : ℕ) ↦ F (x (n + k)) a) atTop (𝓝 (f a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
refine h_lim.mono fun a h_lim => ?_

Premises used: Filter.Eventually.mono
-- 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_1 : ∀ᵐ (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)
a : α
h_lim refine_5 : Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
refine_5₁ : Tendsto (fun (n : ℕ) ↦ x (n + k)) atTop l
refine_5₂ : Filter ι
⊢ Tendsto (fun (n : ℕ) ↦ F (x (n + k)) a) atTop (𝓝 (f a))

Tactic:
apply @Tendsto.comp _ _ _ (fun n => x (n + k)) fun n => F n a

Premises used: Filter.Tendsto.comp
-- 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_1 : ∀ᵐ (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)
a : α
h_lim : Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
⊢ Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))

Tactic:
assumption
-- 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_1 : ∀ᵐ (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)
a : α
h_lim : Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
refine_5 : Tendsto x atTop l
⊢ Tendsto (fun (n : ℕ) ↦ x (n + k)) atTop l

Tactic:
rw [tendsto_add_atTop_iff_nat]

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_1 : ∀ᵐ (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)
a : α
h_lim : Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
⊢ Tendsto x atTop l

Tactic:
assumption
-- 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, Measurable (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))
⊢ Tendsto (fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
tendsto_lintegral_filter_of_dominated_convergence' bound ?_ h_bound h_fin h_lim

Premises used: MeasureTheory.tendsto_lintegral_filter_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, Measurable (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))
refine : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
⊢ Tendsto (fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))

Tactic:
refine tendsto_lintegral_filter_of_dominated_convergence' bound ?_ h_bound h_fin h_lim

Premises used: MeasureTheory.tendsto_lintegral_filter_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, Measurable (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))
⊢ ∀ (a : ι), Measurable (F a) → AEMeasurable (F a) μ

Tactic:
fun_prop
-- 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, Measurable (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))
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ Measurable (F n)) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} x}
      a
h₁ : ∀ (a : ι), Measurable (F a) → AEMeasurable (F a) μ
⊢ ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ

Tactic:
filter_upwards [hF_meas] using by fun_prop
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
a : α
ha : F a < ∞
⊢ F a ≠ ∞

Tactic:
ha.ne

Premises used: LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ F x < ∞) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ F a ≠ ∞) x} x}
      a
h₁ h₂ : ∀ (a : α) (ha : F a < ∞), F a ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, F a ≠ ∞

Tactic:
filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.ne

Premises used: MeasureTheory.ae_lt_top'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, F a ≠ ∞

Tactic:
have h_bound_finite : ∀ᵐ a ∂μ, F a ≠ ∞ := by
    filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.ne
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h :
  ∀ (a : α) (h_le : ∀ (i : ℕ), f i a ≤ F a) (h_fin : F a ≠ ∞) (h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a),
    ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
⊢ ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
filter_upwards [h_bound, h_bound_finite, hf_mono] with a h_le h_fin h_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atTop ∨ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
have h_tendsto : Tendsto (fun i ↦ f i a) atTop atTop ∨
        ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) := tendsto_atTop_of_monotone h_mono
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atTop ∨ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
h :
  ∀ (h_absurd : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atTop),
    ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
h₁ :
  ∀ (h_tendsto : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)),
    ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
rcases h_tendsto with h_absurd | h_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_absurd : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atTop
⊢ ∀ (b : ℝ≥0∞), ∃ (a_1 : ℕ), b ≤ f a_1 a

Tactic:
rw [tendsto_atTop_atTop_iff_of_monotone h_mono] at h_absurd

Premises used: Filter.tendsto_atTop_atTop_iff_of_monotone
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ (a_1 : ℕ), b ≤ f a_1 a
h : ∀ (i : ℕ) (hi : F a + 1 ≤ f i a), ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
obtain ⟨i, hi⟩ := h_absurd (F a + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ (a_1 : ℕ), b ≤ f a_1 a
i : ℕ
hi : F a + 1 ≤ f i a
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
absurd (hi.trans (h_le _)) (not_le.mpr ?_)

Premises used: not_le, Iff.mpr, absurd, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ (a_1 : ℕ), b ≤ f a_1 a
i : ℕ
hi : F a + 1 ≤ f i a
h : F a < F a + 1
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
refine absurd (hi.trans (h_le _)) (not_le.mpr ?_)

Premises used: not_le, Iff.mpr, absurd, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ (a_1 : ℕ), b ≤ f a_1 a
i : ℕ
hi : F a + 1 ≤ f i a
⊢ F a < F a + 1

Tactic:
ENNReal.lt_add_right h_fin one_ne_zero

Premises used: ENNReal.lt_add_right, one_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ (a_1 : ℕ), b ≤ f a_1 a
i : ℕ
hi : F a + 1 ≤ f i a
⊢ F a < F a + 1

Tactic:
exact ENNReal.lt_add_right h_fin one_ne_zero

Premises used: ENNReal.lt_add_right, one_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_tendsto : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
h_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ∞
h_mono : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_tendsto : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
exact h_tendsto