awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
simp_rw : Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α), f i x ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
⊢ Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), g' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))

Tactic:
simp_rw [Int_eq]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α), f i x ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))

Tactic:
hf_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun (i : ℕ) ↦ ∫⁻ (x : α), f i x ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))

Tactic:
exact hf_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ g' i a

Tactic:
Eventually.of_forall (fun x ↦ monotone_nat_of_le_succ (fun n ↦ le_max_right _ _))

Premises used: le_max_right, Filter.Eventually.of_forall, HAdd.hAdd, OfNat.ofNat, monotone_nat_of_le_succ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ g' i a

Tactic:
exact Eventually.of_forall (fun x ↦ monotone_nat_of_le_succ (fun n ↦ le_max_right _ _))

Premises used: Filter.Eventually.of_forall, monotone_nat_of_le_succ
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
x : α
h'x : ∀ (i : ℕ), f i x ≤ F x
hx : ∀ (n : ℕ), g' n x ≤ f n x
n : ℕ
⊢ g' n x ≤ F x

Tactic:
(hx n).trans (h'x n)

Premises used: LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), f i a ≤ F a) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ∀ (n : ℕ), g' n x ≤ f n x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), g' i a ≤ F a) x} x}
            x}
      a
h₁ h₂ : ∀ (x : α) (h'x : ∀ (i : ℕ), f i x ≤ F x) (hx : ∀ (n : ℕ), g' n x ≤ f n x) (n : ℕ), g' n x ≤ F x
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), g' i a ≤ F a

Tactic:
filter_upwards [h_bound, I'] with x h'x hx n using (hx n).trans (h'x n)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ g' i a) atTop (𝓝 (F a))

Tactic:
have : ∀ᵐ a ∂μ, Tendsto (fun i ↦ g' i a) atTop (𝓝 (F a)) := by
    apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite
    · exact fun n ↦ (M n).aemeasurable
    · simp_rw [Int_eq]
      exact hf_tendsto
    · exact Eventually.of_forall (fun x ↦ monotone_nat_of_le_succ (fun n ↦ le_max_right _ _))
    · filter_upwards [h_bound, I'] with x h'x hx n using (hx n).trans (h'x n)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ g' i a) atTop (𝓝 (F a))
h :
  ∀ (x : α) (hx : Tendsto (fun (i : ℕ) ↦ g' i x) atTop (𝓝 (F x))) (h'x : ∀ (n : ℕ), g' n x ≤ f n x)
    (h''x : ∀ (i : ℕ), f i x ≤ F x), Tendsto (fun (i : ℕ) ↦ f i x) atTop (𝓝 (F x))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))

Tactic:
filter_upwards [this, I', h_bound] with x hx h'x h''x
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ g' i a) atTop (𝓝 (F a))
x : α
hx : Tendsto (fun (i : ℕ) ↦ g' i x) atTop (𝓝 (F x))
h'x : ∀ (n : ℕ), g' n x ≤ f n x
h''x : ∀ (i : ℕ), f i x ≤ F x
⊢ Tendsto (fun (i : ℕ) ↦ f i x) atTop (𝓝 (F x))

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le hx tendsto_const_nhds h'x h''x

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : (n : ℕ) → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α → ℝ≥0∞) (g 0) (fun (n : ℕ) (I : α → ℝ≥0∞) (x : α) ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ g' i a) atTop (𝓝 (F a))
x : α
hx : Tendsto (fun (i : ℕ) ↦ g' i x) atTop (𝓝 (F x))
h'x : ∀ (n : ℕ), g' n x ≤ f n x
h''x : ∀ (i : ℕ), f i x ≤ F x
⊢ Tendsto (fun (i : ℕ) ↦ f i x) atTop (𝓝 (F x))

Tactic:
exact tendsto_of_tendsto_of_tendsto_of_le_of_le hx tendsto_const_nhds h'x h''x

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

Tactic:
((lintegral_mono_ae ?_).trans_lt h0.lt_top).ne

Premises used: MeasureTheory.lintegral_mono_ae, Ne.lt_top, LE.le.trans_lt, 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_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
refine : ∀ᵐ (a : α) ∂μ, F a ≤ f 0 a
⊢ ∫⁻ (a : α), F a ∂μ ≠ ∞

Tactic:
refine ((lintegral_mono_ae ?_).trans_lt h0.lt_top).ne

Premises used: MeasureTheory.lintegral_mono_ae, Ne.lt_top, LE.le.trans_lt, 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_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
a : α
ha : ∀ (i : ℕ), F a ≤ f i a
⊢ F a ≤ f 0 a

Tactic:
ha 0

Premises used: 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_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), F a ≤ f i a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ F a ≤ f 0 a) x} x}
      a
h₁ h₂ : ∀ (a : α) (ha : ∀ (i : ℕ), F a ≤ f i a), F a ≤ f 0 a
⊢ ∀ᵐ (a : α) ∂μ, F a ≤ f 0 a

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

Tactic:
have h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞ := by
    refine ((lintegral_mono_ae ?_).trans_lt h0.lt_top).ne
    filter_upwards [h_bound] with a ha using ha 0
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h :
  ∀ (a : α) (h_mono : Antitone (β := ℝ≥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 [hf_mono] with a 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_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
a : α
h_mono : Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h :
  ∀ (h : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atBot), ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
h₁ :
  ∀ (h : ∃ (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 _root_.tendsto_atTop_of_antitone h_mono with h | h

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

Tactic:
⟨0, h.mono_right ?_⟩

Premises used: Exists.intro, Filter.Tendsto.mono_right, 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_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
a : α
h_mono : Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atBot
h₁ : LE.le (α := Filter ℝ≥0∞) atBot (𝓝 0)
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)

Tactic:
refine ⟨0, h.mono_right ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
a : α
h_mono : Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atBot
h₁ : LE.le (α := Filter ℝ≥0∞) (pure ⊥) (𝓝 0)
⊢ LE.le (α := Filter ℝ≥0∞) atBot (𝓝 0)

Tactic:
rw [OrderBot.atBot_eq]

Premises used: Filter.OrderBot.atBot_eq
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
a : α
h_mono : Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atBot
⊢ LE.le (α := Filter ℝ≥0∞) (pure ⊥) (𝓝 0)

Tactic:
pure_le_nhds _

Premises used: Set.Mem, pure_le_nhds
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
a : α
h_mono : Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atBot
⊢ LE.le (α := Filter ℝ≥0∞) (pure ⊥) (𝓝 0)

Tactic:
exact pure_le_nhds _

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

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

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

Tactic:
have h_exists : ∀ᵐ a ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) := by
    filter_upwards [hf_mono] with a h_mono
    rcases _root_.tendsto_atTop_of_antitone h_mono with h | h
    · refine ⟨0, h.mono_right ?_⟩
      rw [OrderBot.atBot_eq]
      exact pure_le_nhds _
    · exact h