awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
Tactic: have h_tendsto : Tendsto (fun i ↦ ∫⁻ a, f' i a ∂μ) atTop (𝓝 (∫⁻ a, F' a ∂μ)) := by
    simp_rw [hf'_int_eq, hF'_int_eq]
    refine (ENNReal.continuous_ofReal.tendsto _).comp ?_
    rwa [tendsto_sub_const_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
⊢ ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
have h : ∀ (a : α) (ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a) ⦃i j : ℕ⦄ (hij : i ≤ j),
  LE.le (α := ℝ≥0∞) ((fun (i : ℕ) ↦ f' i a) i) ((fun (i : ℕ) ↦ f' i a) j)
Tactic: filter_upwards [hf_mono] with a ha_mono i j hij
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
a : α
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := ℝ≥0∞) ((fun (i : ℕ) ↦ f' i a) i) ((fun (i : ℕ) ↦ f' i a) j)
have h : f i a - f 0 a ≤ f j a - f 0 a
Tactic: refine ENNReal.ofReal_le_ofReal ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
Tactic: have h_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f' i a) := by
    filter_upwards [hf_mono] with a ha_mono i j hij
    refine ENNReal.ofReal_le_ofReal ?_
    simp [ha_mono hij]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
have h : ∀ (a : α) (ha_bound : ∀ (i : ℕ), f i a ≤ F a) (i : ℕ), f' i a ≤ F' a
Tactic: filter_upwards [hf_bound] with a ha_bound i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
a : α
ha_bound : ∀ (i : ℕ), f i a ≤ F a
i : ℕ
⊢ f' i a ≤ F' a
have h : f i a - f 0 a ≤ F a - f 0 a
Tactic: refine ENNReal.ofReal_le_ofReal ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
Tactic: have h_bound : ∀ᵐ a ∂μ, ∀ i, f' i a ≤ F' a := by
    filter_upwards [hf_bound] with a ha_bound i
    refine ENNReal.ofReal_le_ofReal ?_
    simp only [tsub_le_iff_right, sub_add_cancel, ha_bound i]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have refine_3 : ∀ (h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))),
  ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
Tactic: have h := tendsto_of_lintegral_tendsto_of_monotone ?_ h_tendsto h_mono h_bound ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
refine_3 :
  ∀ (h : ∀ᵐ (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 refine_1 : AEMeasurable F' μ
Tactic: have h := tendsto_of_lintegral_tendsto_of_monotone ?_ h_tendsto h_mono h_bound ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
refine_3 :
  ∀ (h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))),
    ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
refine_1 : AEMeasurable F' μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have refine_2 : ∫⁻ (a : α), F' a ∂μ ≠ ∞
Tactic: have h := tendsto_of_lintegral_tendsto_of_monotone ?_ h_tendsto h_mono h_bound ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h₁ : ∀ (a : α) (ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))) (ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a)
  (ha_bound : ∀ (i : ℕ), f i a ≤ F a), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
Tactic: filter_upwards [h, hf_mono, hf_bound] with a ha ha_mono ha_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
⊢ Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (ENNReal.ofReal (f i a - f 0 a)).toReal + f 0 a
have h₁ : ∀ (i : ℕ), f i a = (ENNReal.ofReal (f i a - f 0 a)).toReal + f 0 a
Tactic: ext i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
i : ℕ
⊢ f i a = (ENNReal.ofReal (f i a - f 0 a)).toReal + f 0 a
have h₁ : f i a = f i a - f 0 a + f 0 a
Tactic: rw [ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
i : ℕ
h₁ : f i a = f i a - f 0 a + f 0 a
⊢ f i a = (ENNReal.ofReal (f i a - f 0 a)).toReal + f 0 a
have h₂ : 0 ≤ f i a - f 0 a
Tactic: rw [ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
Tactic: have h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a := by
    unfold f'
    ext i
    rw [ENNReal.toReal_ofReal]
    · abel
    · simp [ha_mono zero_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
⊢ F a = (ENNReal.ofReal (F a - f 0 a)).toReal + f 0 a
have rw : F a = F a - f 0 a + f 0 a
Tactic: rw [ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
rw : F a = F a - f 0 a + f 0 a
⊢ F a = (ENNReal.ofReal (F a - f 0 a)).toReal + f 0 a
have rw₁ : 0 ≤ F a - f 0 a
Tactic: rw [ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun (n : ℕ) (a : α) ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun (a : α) ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h2 : F a = (F' a).toReal + f 0 a
Tactic: have h2 : F a = (F' a).toReal + f 0 a := by
    unfold F'
    rw [ENNReal.toReal_ofReal]
    · abel
    · simp [ha_bound 0]