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 : ∀ (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_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
let let₁ let₂ : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
let₃ :
  let 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 ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))),
    ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have let₄ : let 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 ∞;
∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))), F' =ᶠ[ae μ] F
Tactic: classical
  let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
    then h.choose else ∞
  have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
    filter_upwards [h_exists] with a ha
    simp_rw [F', dif_pos ha]
    exact ha.choose_spec
  suffices F' =ᵐ[μ] F by
    filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
  have hF'_le : F' ≤ᵐ[μ] F := by
    filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
    exact le_of_tendsto' h_tendsto (fun m ↦ h_le _)
  suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
    ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le
  refine tendsto_nhds_unique ?_ hf_tendsto
  exact lintegral_tendsto_of_tendsto_of_monotone hf_meas hf_mono hF'_tendsto
-- 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_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_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
let let₁ let₂ : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
let₃ :
  let 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 ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))),
    ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
let₄ :
  let 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 ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))), F' =ᶠ[ae μ] F
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have let₅ : let 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 ∞;
∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))) (hF'_le : F' ≤ᶠ[ae μ] F), F' =ᶠ[ae μ] F
Tactic: classical
  let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
    then h.choose else ∞
  have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
    filter_upwards [h_exists] with a ha
    simp_rw [F', dif_pos ha]
    exact ha.choose_spec
  suffices F' =ᵐ[μ] F by
    filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
  have hF'_le : F' ≤ᵐ[μ] F := by
    filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
    exact le_of_tendsto' h_tendsto (fun m ↦ h_le _)
  suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
    ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le
  refine tendsto_nhds_unique ?_ hf_tendsto
  exact lintegral_tendsto_of_tendsto_of_monotone hf_meas hf_mono hF'_tendsto
-- 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_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_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
let let₁ let₂ : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
let₃ :
  let 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 ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))),
    ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
let₄ :
  let 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 ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))), F' =ᶠ[ae μ] F
let₅ :
  let 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 ∞;
  ∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))) (hF'_le : F' ≤ᶠ[ae μ] F),
    F' =ᶠ[ae μ] F
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have let₆ : let 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 ∞;
∀ (hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))) (hF'_le : F' ≤ᶠ[ae μ] F),
  ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ
Tactic: classical
  let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
    then h.choose else ∞
  have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
    filter_upwards [h_exists] with a ha
    simp_rw [F', dif_pos ha]
    exact ha.choose_spec
  suffices F' =ᵐ[μ] F by
    filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
  have hF'_le : F' ≤ᵐ[μ] F := by
    filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
    exact le_of_tendsto' h_tendsto (fun m ↦ h_le _)
  suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
    ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le
  refine tendsto_nhds_unique ?_ hf_tendsto
  exact lintegral_tendsto_of_tendsto_of_monotone hf_meas hf_mono hF'_tendsto
-- 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 ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have this : ∀ (n : ℕ), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f n ∧ ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g a ∂μ
Tactic: have : ∀ n, ∃ g : α → ℝ≥0∞, Measurable g ∧ g ≤ f n ∧ ∫⁻ a, f n a ∂μ = ∫⁻ a, g a ∂μ :=
    fun n ↦ exists_measurable_le_lintegral_eq _ _
-- 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 ∂μ ≠ ∞
this : ∀ (n : ℕ), ∃ (g : α → ℝ≥0∞), Measurable g ∧ g ≤ f n ∧ ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have choose : ∀ (g : (n : ℕ) → α → ℝ≥0∞) (gmeas : ∀ (n : ℕ), Measurable (g n)) (gf : ∀ (n : ℕ), g n ≤ f n)
  (hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ),
  ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
Tactic: choose g gmeas gf hg using this
Cleared hypotheses: this
-- 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
n : ℕ
⊢ Measurable (g' n)
have zero : Measurable (g' 0)
Tactic: induction n with
    | zero => simp [g', gmeas 0]
    | succ n ih => exact Measurable.max (gmeas (n + 1)) ih
Cleared hypotheses: 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
n : ℕ
zero : Measurable (g' 0)
⊢ Measurable (g' n)
have succ : ∀ (n : ℕ) (ih : Measurable (g' n)), Measurable (g' (n + 1))
Tactic: induction n with
    | zero => simp [g', gmeas 0]
    | succ n ih => exact Measurable.max (gmeas (n + 1)) ih
Cleared hypotheses: 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
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have M : ∀ (n : ℕ), Measurable (g' n)
Tactic: have M n : Measurable (g' n) := by
    induction n with
    | zero => simp [g', gmeas 0]
    | succ n ih => exact Measurable.max (gmeas (n + 1)) ih
-- 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)
n : ℕ
x : α
⊢ g n x ≤ g' n x
have zero : g 0 x ≤ g' 0 x
Tactic: cases n with | zero | succ => simp [g']
Cleared hypotheses: 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)
n : ℕ
x : α
zero : g 0 x ≤ g' 0 x
⊢ g n x ≤ g' n x
have succ : ∀ (n : ℕ), g (n + 1) x ≤ g' (n + 1) x
Tactic: cases n with | zero | succ => simp [g']
Cleared hypotheses: 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)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
Tactic: have I : ∀ n x, g n x ≤ g' n x := by
    intro n x
    cases n with | zero | succ => simp [g']
-- 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
⊢ ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
have h : ∀ (x : α) (hx : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i x) (n : ℕ), g' n x ≤ f n x
Tactic: filter_upwards [hf_mono] with x 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
x : α
hx : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i x
n : ℕ
⊢ g' n x ≤ f n x
have h : g' 0 x ≤ f 0 x
Tactic: induction n with
    | zero => simpa [g'] using gf 0 x
    | succ n ih => exact max_le (gf (n + 1) x) (ih.trans (hx (Nat.le_succ n)))
Cleared hypotheses: 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
x : α
hx : Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i x
n : ℕ
h : g' 0 x ≤ f 0 x
⊢ g' n x ≤ f n x
have h₁ : ∀ (n : ℕ) (ih : g' n x ≤ f n x), g' (n + 1) x ≤ f (n + 1) x
Tactic: induction n with
    | zero => simpa [g'] using gf 0 x
    | succ n ih => exact max_le (gf (n + 1) x) (ih.trans (hx (Nat.le_succ n)))
Cleared hypotheses: 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
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Tactic: have I' : ∀ᵐ x ∂μ, ∀ n, g' n x ≤ f n x := by
    filter_upwards [hf_mono] with x hx n
    induction n with
    | zero => simpa [g'] using gf 0 x
    | succ n ih => exact max_le (gf (n + 1) x) (ih.trans (hx (Nat.le_succ 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 : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
have a : ∫⁻ (x : α), g' n x ∂μ ≤ ∫⁻ (x : α), f n x ∂μ
Tactic: apply le_antisymm
-- 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 : ℕ
a : ∫⁻ (x : α), g' n x ∂μ ≤ ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
have a₁ : ∫⁻ (x : α), f n x ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ
Tactic: apply le_antisymm
-- 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 : α), g' n x ∂μ ≤ ∫⁻ (x : α), f n x ∂μ
have a : ∀ᵐ (a : α) ∂μ, g' n a ≤ f n a
Tactic: apply lintegral_mono_ae
-- 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 : ℕ
⊢ ∀ᵐ (a : α) ∂μ, g' n a ≤ f n a
have 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
Tactic: filter_upwards [I'] with x hx using hx n