awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ∂μ ≠ ∞
have refine_3 : ∀ᵐ (a : α) ∂μ, ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ≤ g a
Tactic: refine ne_top_of_le_ne_top h_fin (lintegral_mono_ae ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i a ≤ g a
have refine_3 : ∀ (n : α) (hn : ∀ (i : ℕ), f i n ≤ g n), ⨆ (i : ℕ), ⨆ (_ : i ≥ 0), f i n ≤ g n
Tactic: refine (ae_all_iff.2 h_bound).mono fun n hn => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), F n a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) sorry a ∂μ
Tactic: have : ∀ n, ∫⁻ a, F n a ∂μ = ∫⁻ a, (hF_meas n).mk (F n) a ∂μ := fun n =>
    lintegral_congr_ae (hF_meas n).ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), F n a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have simp_rw : Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), AEMeasurable.mk (F n) sorry a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have tendsto_lintegral_of_dominated_convergence : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) sorry a) atTop (𝓝 (f a))
Tactic: apply
    tendsto_lintegral_of_dominated_convergence bound (fun n => (hF_meas n).measurable_mk) _ h_fin
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
tendsto_lintegral_of_dominated_convergence :
  ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have tendsto_lintegral_of_dominated_convergence₁ : ∀ (n : ℕ), AEMeasurable.mk (F n) sorry ≤ᶠ[ae μ] bound
Tactic: apply
    tendsto_lintegral_of_dominated_convergence bound (fun n => (hF_meas n).measurable_mk) _ h_fin
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))
have this₁ : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) sorry a = F n a
Tactic: have : ∀ n, ∀ᵐ a ∂μ, (hF_meas n).mk (F n) a = F n a := fun n => (hF_meas n).ae_eq_mk.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this_1 : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))
have this₁ : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) sorry a = F n a
Tactic: have : ∀ᵐ a ∂μ, ∀ n, (hF_meas n).mk (F n) a = F n a := ae_all_iff.mpr this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this_1 : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
this_2 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (F n) ⋯ a = F n a
this : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), AEMeasurable.mk (F n) ⋯ a = F n a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) ⋯ a) atTop (𝓝 (f a))
have h : ∀ (a : α) (H : ∀ (n : ℕ), AEMeasurable.mk (F n) sorry a = F n a) (H' : Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))),
  Tendsto (fun (n : ℕ) ↦ AEMeasurable.mk (F n) sorry a) atTop (𝓝 (f a))
Tactic: filter_upwards [this, h_lim] with a H H'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
n : ℕ
⊢ AEMeasurable.mk (F n) ⋯ ≤ᶠ[ae μ] bound
have h : ∀ (a : α) (H : F n a ≤ bound a) (H' : F n a = AEMeasurable.mk (F n) sorry a), AEMeasurable.mk (F n) sorry a ≤ bound a
Tactic: filter_upwards [h_bound n, (hF_meas n).ae_eq_mk] with a H H'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
F : ℕ → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ (n : ℕ), AEMeasurable (F n) μ
h_bound : ∀ (n : ℕ), F n ≤ᶠ[ae μ] bound
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F n a) atTop (𝓝 (f a))
this : ∀ (n : ℕ), ∫⁻ (a : α), F n a ∂μ = ∫⁻ (a : α), AEMeasurable.mk (F n) ⋯ a ∂μ
n : ℕ
a : α
H : F n a ≤ bound a
H' : F n a = AEMeasurable.mk (F n) ⋯ a
⊢ AEMeasurable.mk (F n) ⋯ a ≤ bound a
have h : ∀ (H : AEMeasurable.mk (F n) sorry a ≤ bound a) (H' : F n a = AEMeasurable.mk (F n) sorry a),
  AEMeasurable.mk (F n) sorry a ≤ bound a
Tactic: rwa [H'] at H
Cleared hypotheses: H, H'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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))
⊢ Tendsto (fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))
have rw : ∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
Tactic: rw [tendsto_iff_seq_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
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
⊢ Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
Tactic: have hxl := by
    rw [tendsto_atTop'] at xl
    exact xl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
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
⊢ Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have h : {x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x} ∈ l
Tactic: have h := inter_mem hF_meas h_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h : {x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x} ∈ l
⊢ Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have h₁ : ∃ (a : ℕ),
  ∀ b ≥ a,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
Tactic: replace h := hxl _ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h :
  ∃ (a : ℕ),
    ∀ b ≥ a,
      Membership.mem (γ := Set ι)
        ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
        (x b)
⊢ Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have rcases : ∀ (k : ℕ)
  (h :
    ∀ b ≥ k,
      Membership.mem (γ := Set ι)
        ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
        (x b)),
  Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
Tactic: rcases h with ⟨k, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
⊢ Tendsto ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have rw : Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
Tactic: rw [← tendsto_add_atTop_iff_nat k]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
refine_1 : α → ℝ≥0∞
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have refine_2 : ∀ (n : ℕ), AEMeasurable (F (x (n + k))) μ
Tactic: refine tendsto_lintegral_of_dominated_convergence' ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
refine_1 : α → ℝ≥0∞
refine_2 : ∀ (n : ℕ), AEMeasurable (F (x (n + k))) μ
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have refine_3 : ∀ (n : ℕ), F (x (n + k)) ≤ᶠ[ae μ] bound
Tactic: refine tendsto_lintegral_of_dominated_convergence' ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
refine_1 : α → ℝ≥0∞
refine_2 : ∀ (n : ℕ), AEMeasurable (F (x (n + k))) μ
refine_3 : ∀ (n : ℕ), F (x (n + k)) ≤ᶠ[ae μ] bound
refine_4 : ∫⁻ (a : α), bound a ∂μ ≠ ∞
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have refine_5 : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ F (x (n + k)) a) atTop (𝓝 (f a))
Tactic: refine tendsto_lintegral_of_dominated_convergence' ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
ι : Type u_2
l : Filter ι
inst_1 : l.IsCountablyGenerated
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : ∫⁻ (a : α), bound a ∂μ ≠ ∞
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEMeasurable (F n) μ) x} ∩ {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x})
      (x b)
n : ℕ
⊢ AEMeasurable (F (x (n + k))) μ
have refine_2 : n + k ≥ k
Tactic: refine (h _ ?_).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
have refine_3 : n + k ≥ k
Tactic: refine (h _ ?_).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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))
have 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))
Tactic: refine h_lim.mono fun a h_lim => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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))
⊢ Tendsto (fun (n : ℕ) ↦ F (x (n + k)) a) atTop (𝓝 (f a))
have refine_5₁ : Tendsto (fun (n : ℕ) ↦ x (n + k)) atTop l
Tactic: apply @Tendsto.comp _ _ _ (fun n => x (n + k)) fun n => F n a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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 ∂μ))
have refine : ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
Tactic: refine tendsto_lintegral_filter_of_dominated_convergence' bound ?_ h_bound h_fin h_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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))
⊢ ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
have 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
Tactic: filter_upwards [hF_meas] using by fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence (goal)
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
⊢ ∀ᶠ (n : ι) in l, AEMeasurable (F n) μ
have h₁ : ∀ (a : ι), Measurable (F a) → AEMeasurable (F a) μ
Tactic: filter_upwards [hF_meas] using by fun_prop
-- 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 ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, F a ≠ ∞
have 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
Tactic: filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.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_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
⊢ ∀ᵐ (a : α) ∂μ, F a ≠ ∞
have h₁ : ∀ (a : α), F a < ∞ → F a ≠ ∞
Tactic: filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.ne