awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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)
i : ℕ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ f i a - f 0 a) μ

Tactic:
exact (hf_int i).sub (hf_int 0)

Premises used: MeasureTheory.Integrable.sub, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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)
i : ℕ
h : ∀ (a : α) (h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a), 0 a ≤ f i a - f 0 a
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ f i a - f 0 a

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

Tactic:
simp [h_mono zero_le]

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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)
⊢ ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))

Tactic:
have hf'_int_eq : ∀ i, ∫⁻ a, f' i a ∂μ = ENNReal.ofReal (∫ a, f i a ∂μ - ∫ a, f 0 a ∂μ) := by
    intro i
    unfold f'
    rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub (hf_int i) (hf_int 0)]
    · exact (hf_int i).sub (hf_int 0)
    · filter_upwards [hf_mono] with a h_mono
      simp [h_mono zero_le]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
unfold :
  ∫⁻ (a : α), ENNReal.ofReal (F a - f 0 a) ∂μ =
    ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
⊢ ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))

Tactic:
unfold F'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
hfi : Integrable (ε := ℝ) (fun (a : α) ↦ F a - f 0 a) μ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ F a - f 0 a
⊢ ∫⁻ (a : α), ENNReal.ofReal (F a - f 0 a) ∂μ =
    ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub hF_int (hf_int 0)]

Premises used: MeasureTheory.integral_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_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 ∂μ))
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ F a - f 0 a) μ

Tactic:
hF_int.sub (hf_int 0)

Premises used: MeasureTheory.Integrable.sub, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ F a - f 0 a) μ

Tactic:
exact hF_int.sub (hf_int 0)

Premises used: MeasureTheory.Integrable.sub, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
h : ∀ (a : α) (h_bound : ∀ (i : ℕ), f i a ≤ F a), 0 a ≤ F a - f 0 a
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ F a - f 0 a

Tactic:
filter_upwards [hf_bound] with a h_bound
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
a : α
h_bound : ∀ (i : ℕ), f i a ≤ F a
⊢ 0 a ≤ F a - f 0 a

Tactic:
simp [h_bound 0]

Premises used: OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
⊢ ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))

Tactic:
have hF'_int_eq : ∫⁻ a, F' a ∂μ = ENNReal.ofReal (∫ a, F a ∂μ - ∫ a, f 0 a ∂μ) := by
    unfold F'
    rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub hF_int (hf_int 0)]
    · exact hF_int.sub (hf_int 0)
    · filter_upwards [hf_bound] with a h_bound
      simp [h_bound 0]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
simp_rw :
  Tendsto (fun (i : ℕ) ↦ ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))) atTop
    (𝓝 (ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))))
⊢ Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))

Tactic:
simp_rw [hf'_int_eq, hF'_int_eq]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
⊢ Tendsto (fun (i : ℕ) ↦ ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))) atTop
    (𝓝 (ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))))

Tactic:
(ENNReal.continuous_ofReal.tendsto _).comp ?_

Premises used: ENNReal.ofNNReal, ENNReal.ofReal, ENNReal.continuous_ofReal, WithTop.some, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
refine :
  Tendsto (fun (i : ℕ) ↦ HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ)) atTop
    (𝓝 (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ)))
⊢ Tendsto (fun (i : ℕ) ↦ ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))) atTop
    (𝓝 (ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))))

Tactic:
refine (ENNReal.continuous_ofReal.tendsto _).comp ?_

Premises used: ENNReal.continuous_ofReal, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
rwa rwa₁ rwa₂ rwa₃ : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
⊢ Tendsto (fun (i : ℕ) ↦ HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ)) atTop
    (𝓝 (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ)))

Tactic:
rwa [tendsto_sub_const_iff]

Premises used: Filter.tendsto_sub_const_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ))
⊢ 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]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 :
  ∀ (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)
⊢ ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a

Tactic:
filter_upwards [hf_mono] with a ha_mono i j hij
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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)

Tactic:
ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
h : f i a - f 0 a ≤ f j a - f 0 a
⊢ LE.le (α := ℝ≥0∞) ((fun (i : ℕ) ↦ f' i a) i) ((fun (i : ℕ) ↦ f' i a) j)

Tactic:
refine ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
⊢ f i a - f 0 a ≤ f j a - f 0 a

Tactic:
simp [ha_mono hij]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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

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

Tactic:
filter_upwards [hf_bound] with a ha_bound i
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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

Tactic:
ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 : ℕ
h : f i a - f 0 a ≤ F a - f 0 a
⊢ f' i a ≤ F' a

Tactic:
refine ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal