awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_le : Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α), (g - f) x ∂μ) 0

Tactic:
simpa [Pi.sub_apply, integral_sub hg hf, sub_eq_zero, eq_comm]

Premises used: sub_eq_zero, MeasureTheory.integral_sub, eq_comm, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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∞)
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∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥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]

Premises used: Pi.zero_apply, Filter.EventuallyEq, Ne, eq_comm, MeasureTheory.ae_iff, MeasureTheory.integral_nonneg_of_ae, MeasureTheory.integral_eq_zero_iff_of_nonneg_ae, Function.support, LE.le.lt_iff_ne, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ f
hfi : Integrable f μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)

Tactic:
integral_pos_iff_support_of_nonneg_ae (Eventually.of_forall hf) hfi

Premises used: MeasureTheory.integral_pos_iff_support_of_nonneg_ae, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ Real.exp (f x)) μ
rw :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), Real.exp (f x) ∂μ)

Tactic:
rw [integral_pos_iff_support_of_nonneg (fun x ↦ (Real.exp_pos _).le) hf]

Premises used: LT.lt.le, MeasureTheory.integral_pos_iff_support_of_nonneg, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ Real.exp (f x)) μ
this : Eq.{u_1 + 1} (α := Set α) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) univ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) : ℝ≥0∞)

Tactic:
simp [this, hμ.out]

Premises used: NeZero.out
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ Real.exp (f x)) μ
suffices : Eq.{u_1 + 1} (α := Set α) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) univ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) : ℝ≥0∞)

Tactic:
suffices (Function.support fun x ↦ Real.exp (f x)) = Set.univ by simp [this, hμ.out]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ Real.exp (f x)) μ
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) x ↔
      Membership.mem (γ := Set α) univ x
⊢ Eq.{u_1 + 1} (α := Set α) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) univ

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ Real.exp (f x)) μ
x : α
⊢ Membership.mem (γ := Set α) (Function.support (M := ℝ) fun (x : α) ↦ Real.exp (f x)) x ↔
    Membership.mem (γ := Set α) univ x

Tactic:
simp only [Function.mem_support, ne_eq, (Real.exp_pos _).ne', not_false_eq_true, Set.mem_univ]

Premises used: ne_eq, LT.lt.ne', Set.mem_univ, Function.mem_support, not_false_eq_true, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
h : ∀ (a : α) (ha : Monotone (β := ℝ) fun (n : ℕ) ↦ f n a) (n : ℕ), 0 ≤ f' n a
⊢ ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x

Tactic:
filter_upwards [h_mono] with a ha n
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
a : α
ha : Monotone (β := ℝ) fun (n : ℕ) ↦ f n a
n : ℕ
⊢ 0 ≤ f' n a

Tactic:
simp [f', ha zero_le]

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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

Tactic:
have hf'_nonneg : ∀ᵐ x ∂μ, ∀ n, 0 ≤ f' n x := by
    filter_upwards [h_mono] with a ha n
    simp [f', ha zero_le]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
⊢ ∀ (n : ℕ), Integrable (f' n) μ

Tactic:
have hf'_meas : ∀ n, Integrable (f' n) μ := fun n ↦ (hf n).sub (hf 0)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (a : α), f x a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))

Tactic:
simp_rw [f', integral_sub (hf _) (hf _), integral_sub' hF (hf 0),
      tendsto_sub_const_iff] at this

Premises used: MeasureTheory.integral_sub, Filter.tendsto_sub_const_iff, MeasureTheory.integral_sub', OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
this : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (a : α), f x a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
this
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
this : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (a : α), f x a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
exact this
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
suffices : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F 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
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
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
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x

Tactic:
filter_upwards [h_tendsto, h_mono] with x hx_tendsto hx_mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
h : f 0 x ≤ F x
⊢ 0 x ≤ (F - f 0) x

Tactic:
simp only [Pi.zero_apply, Pi.sub_apply, sub_nonneg]

Premises used: Pi.zero_apply, sub_nonneg, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
⊢ f 0 x ≤ F x

Tactic:
ge_of_tendsto' hx_tendsto (fun n ↦ hx_mono zero_le)

Premises used: zero_le, ge_of_tendsto'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
⊢ f 0 x ≤ F x

Tactic:
exact ge_of_tendsto' hx_tendsto (fun n ↦ hx_mono zero_le)

Premises used: zero_le, ge_of_tendsto'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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

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)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a

Tactic:
rw [ae_all_iff] at hf'_nonneg

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
hf'_nonneg₁ : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
⊢ ∀ (n : ℕ), Integrable (f' n) μ

Tactic:
rw [ae_all_iff] at hf'_nonneg

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
hf'_nonneg₁ : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas₁ : ∀ (n : ℕ), Integrable (f' n) μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x

Tactic:
rw [ae_all_iff] at hf'_nonneg

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
simp_rw :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae (hf'_nonneg _) (hf'_meas _).1]

Premises used: And.left, MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
rw :
  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 (𝓝 (∫ (x : α), (F - f 0) x ∂μ))

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae hF_ge (hF.1.sub (hf 0).1)]

Premises used: MeasureTheory.AEStronglyMeasurable.sub, And.left, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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)
refine_1 : ∫⁻ (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) ∂μ) ?_
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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_1 : ENNReal.ofReal (∫ (x : α), (F - f 0) x ∂μ) ≠ ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ ≠ ∞

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (hF.sub (hf 0)) hF_ge]

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.ofReal_integral_eq_lintegral_ofReal, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
⊢ ENNReal.ofReal (∫ (x : α), (F - f 0) x ∂μ) ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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)

Tactic:
h_cont.tendsto.comp ?_

Premises used: ENNReal.toReal, ContinuousAt.tendsto, Filter.Tendsto.comp, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 :
  Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ) atTop (𝓝 (∫⁻ (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:
refine h_cont.tendsto.comp ?_

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) ∂μ))

Tactic:
lintegral_tendsto_of_tendsto_of_monotone ?_ ?_ ?_

Premises used: MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone