awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
n : ℕ
h :
  ∀ (a : α),
    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 : α) ↦ g' n a ≤ f n a) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μ, g' n a ≤ f n a
have h₁ : ∀ (a : α), (∀ (n : ℕ), g' n a ≤ f n a) → g' n a ≤ f n a
Tactic: filter_upwards [I'] with x hx using hx n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
n : ℕ
⊢ ∫⁻ (x : α), f n x ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ
have a : ∫⁻ (a : α), g n a ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ
Tactic: rw [hg n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
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
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
Tactic: have Int_eq n : ∫⁻ x, g' n x ∂μ = ∫⁻ x, f n x ∂μ := by
    apply le_antisymm
    · apply lintegral_mono_ae
      filter_upwards [I'] with x hx using hx n
    · rw [hg n]
      exact lintegral_mono (I n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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))
have apply : ∀ (n : ℕ), AEMeasurable (g' n) μ
Tactic: apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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 ∂μ
apply : ∀ (n : ℕ), AEMeasurable (g' n) μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ g' i a) atTop (𝓝 (F a))
have apply₁ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), g' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
Tactic: apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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 ∂μ
apply : ∀ (n : ℕ), AEMeasurable (g' n) μ
apply₁ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), g' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ g' i a) atTop (𝓝 (F a))
have apply₂ : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ g' i a
Tactic: apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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 ∂μ
apply : ∀ (n : ℕ), AEMeasurable (g' n) μ
apply₁ : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), g' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
apply₂ : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ g' i a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ g' i a) atTop (𝓝 (F a))
have apply₃ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), g' i a ≤ F a
Tactic: apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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 : α) ∂μ, ∀ (i : ℕ), g' i a ≤ F a
have 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
Tactic: filter_upwards [h_bound, I'] with x h'x hx n using (hx n).trans (h'x n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), g' i a ≤ F a
have h₁ : ∀ (a : α), (∀ (i : ℕ), f i a ≤ F a) → (∀ (n : ℕ), g' n a ≤ f n 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
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 : ℕ) ↦ f i a) atTop (𝓝 (F a))
have this : ∀ᵐ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have 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))
Tactic: filter_upwards [this, I', h_bound] with x hx h'x h''x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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 ∂μ ≠ ∞
have refine : ∀ᵐ (a : α) ∂μ, F a ≤ f 0 a
Tactic: refine ((lintegral_mono_ae ?_).trans_lt h0.lt_top).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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 ≤ f 0 a
have 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
Tactic: filter_upwards [h_bound] with a ha using ha 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
⊢ ∀ᵐ (a : α) ∂μ, F a ≤ f 0 a
have h₁ : ∀ (a : α), (∀ (i : ℕ), F a ≤ f i a) → F a ≤ f 0 a
Tactic: filter_upwards [h_bound] with a ha using ha 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
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 : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h_int_finite : ∫⁻ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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)
have h : ∀ (a : α) (h_mono : Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a), ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
Tactic: filter_upwards [hf_mono] with a h_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
have h : ∀ (h : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ f i a) atTop atBot), ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
Tactic: rcases _root_.tendsto_atTop_of_antitone h_mono with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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)
⊢ ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
have h₁ : ∀ (h : ∃ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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)
have h₁ : LE.le (α := Filter ℝ≥0∞) atBot (𝓝 0)
Tactic: refine ⟨0, h.mono_right ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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∞) atBot (𝓝 0)
have h₁ : LE.le (α := Filter ℝ≥0∞) (pure ⊥) (𝓝 0)
Tactic: rw [OrderBot.atBot_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
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 : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h_exists : ∀ᵐ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
have h : ∀ (a : α) (ha : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
Tactic: filter_upwards [h_exists] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
a : α
ha : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
have h : Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (ha.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))))
Tactic: simp_rw [F', dif_pos ha]