awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
simp_rw :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
simp_rw₁ :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
have simp_rw₂ : ¬Eq (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
simp_rw :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
simp_rw₁ :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  ¬Eq (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
have simp_rw₃ : ¬Eq (α := ℝ) (∫ (x : α), f x ∂μ) 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
simp_rw :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
simp_rw₁ :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  ¬Eq (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₃ :
  ¬Eq (α := ℝ) (∫ (x : α), f x ∂μ) 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
have simp_rw₄ : ¬f =ᶠ[ae μ] 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
simp_rw :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
simp_rw₁ :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  ¬Eq (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₃ :
  ¬Eq (α := ℝ) (∫ (x : α), f x ∂μ) 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₄ : ¬f =ᶠ[ae μ] 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
have simp_rw₅ : (¬∀ᵐ (x : α) ∂μ, f x = 0 x) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
simp_rw :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
simp_rw₁ :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  ¬Eq (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₃ :
  ¬Eq (α := ℝ) (∫ (x : α), f x ∂μ) 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₄ : ¬f =ᶠ[ae μ] 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₅ :
  (¬∀ᵐ (x : α) ∂μ, f x = 0 x) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
have simp_rw₆ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = 0 a} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
simp_rw :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
simp_rw₁ :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  ¬Eq (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₃ :
  ¬Eq (α := ℝ) (∫ (x : α), f x ∂μ) 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₄ : ¬f =ᶠ[ae μ] 0 ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₅ :
  (¬∀ᵐ (x : α) ∂μ, f x = 0 x) ↔ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₆ :
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = 0 a} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
have simp_rw₇ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = 0} : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ Real.exp (f x)) μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), Real.exp (f x) ∂μ)
have rw : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) : ℝ≥0∞)
Tactic: rw [integral_pos_iff_support_of_nonneg (fun x ↦ (Real.exp_pos _).le) hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ Real.exp (f x)) μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) : ℝ≥0∞)
have suffices : Eq.{u_1 + 1} (α := Set α) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) univ
Tactic: suffices (Function.support fun x ↦ Real.exp (f x)) = Set.univ by simp [this, hμ.out]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ Real.exp (f x)) μ
⊢ Eq.{u_1 + 1} (α := Set α) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) univ
have h : ∀ (x : α),
  Membership.mem (γ := Set α) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) x ↔
    Membership.mem (γ := Set α) univ x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
⊢ ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
have h : ∀ (a : α) (ha : Monotone (β := ℝ) fun (n : ℕ) ↦ f n a) (n : ℕ), 0 ≤ f' n a
Tactic: filter_upwards [h_mono] with a ha n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))
have hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
Tactic: have hf'_nonneg : ∀ᵐ x ∂μ, ∀ n, 0 ≤ f' n x := by
    filter_upwards [h_mono] with a ha n
    simp [f', ha zero_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))
have hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
Tactic: have hf'_meas : ∀ n, Integrable (f' n) μ := fun n ↦ (hf n).sub (hf 0)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))
have suffices : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
Tactic: suffices Tendsto (fun n ↦ ∫ x, f' n x ∂μ) atTop (𝓝 (∫ x, (F - f 0) x ∂μ)) by
    simp_rw [f', integral_sub (hf _) (hf _), integral_sub' hF (hf 0),
      tendsto_sub_const_iff] at this
    exact this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
have h : ∀ (x : α) (hx_tendsto : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x)))
  (hx_mono : Monotone (β := ℝ) fun (n : ℕ) ↦ f n x), 0 x ≤ (F - f 0) x
Tactic: filter_upwards [h_tendsto, h_mono] with x hx_tendsto hx_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
x : α
hx_tendsto : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
hx_mono : Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
⊢ 0 x ≤ (F - f 0) x
have h : f 0 x ≤ F x
Tactic: simp only [Pi.zero_apply, Pi.sub_apply, sub_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
have hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
Tactic: have hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x := by
    filter_upwards [h_tendsto, h_mono] with x hx_tendsto hx_mono
    simp only [Pi.zero_apply, Pi.sub_apply, sub_nonneg]
    exact ge_of_tendsto' hx_tendsto (fun n ↦ hx_mono zero_le)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
have hf'_nonneg₁ : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
Tactic: rw [ae_all_iff] at hf'_nonneg
Cleared hypotheses: hf'_nonneg, hf'_meas, hF_ge
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
have simp_rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
Tactic: simp_rw [integral_eq_lintegral_of_nonneg_ae (hf'_nonneg _) (hf'_meas _).1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
have rw : Tendsto (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
  (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
Tactic: rw [integral_eq_lintegral_of_nonneg_ae hF_ge (hF.1.sub (hf 0).1)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
⊢ Tendsto (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
    (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
have refine_2 : ∀ (h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)),
  Tendsto (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
    (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
Tactic: have h_cont := ENNReal.continuousAt_toReal (x := ∫⁻ a, ENNReal.ofReal ((F - f 0) a) ∂μ) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
refine_2 :
  ∀ (h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)),
    Tendsto (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
      (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
⊢ Tendsto (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
    (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
have refine_1 : ∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ ≠ ∞
Tactic: have h_cont := ENNReal.continuousAt_toReal (x := ∫⁻ a, ENNReal.ofReal ((F - f 0) a) ∂μ) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
⊢ ∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ ≠ ∞
have refine_1 : ENNReal.ofReal (∫ (x : α), (F - f 0) x ∂μ) ≠ ∞
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal (hF.sub (hf 0)) hF_ge]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ Tendsto (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
    (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)
have refine_2 : Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ))
Tactic: refine h_cont.tendsto.comp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ))
have refine_2 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f' n a)) μ
Tactic: refine lintegral_tendsto_of_tendsto_of_monotone ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
refine_2 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f' n a)) μ
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ))
have refine_2₁ : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)
Tactic: refine lintegral_tendsto_of_tendsto_of_monotone ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
refine_2 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f' n a)) μ
refine_2₁ : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ))
have refine_2₂ : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))
Tactic: refine lintegral_tendsto_of_tendsto_of_monotone ?_ ?_ ?_