awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f' n a)) μ
refine_2₁ : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)
refine_2₂ : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ))

Tactic:
refine lintegral_tendsto_of_tendsto_of_monotone ?_ ?_ ?_

Premises used: MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone
-- 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) ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f' n a)) μ

Tactic:
fun n ↦ ((hf n).sub (hf 0)).aemeasurable.ennreal_ofReal

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.Integrable.aemeasurable, AEMeasurable.ennreal_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
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f' n a)) μ

Tactic:
exact fun n ↦ ((hf n).sub (hf 0)).aemeasurable.ennreal_ofReal

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.Integrable.aemeasurable, AEMeasurable.ennreal_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
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
h :
  ∀ (x : α) (hx : Monotone (β := ℝ) fun (n : ℕ) ↦ f n x) ⦃n m : ℕ⦄ (hnm : n ≤ m),
    LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) n) ((fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) m)
⊢ ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)

Tactic:
filter_upwards [h_mono] with x hx n m hnm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m_1 : 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) ∂μ)
x : α
hx : Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
n m : ℕ
hnm : n ≤ m
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) n) ((fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) m)

Tactic:
ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m_1 : 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) ∂μ)
x : α
hx : Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
n m : ℕ
hnm : n ≤ m
h : f' n x ≤ f' m x
⊢ LE.le (α := ℝ≥0∞) ((fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) n) ((fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) m)

Tactic:
refine ENNReal.ofReal_le_ofReal ?_

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m_1 : 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) ∂μ)
x : α
hx : Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
n m : ℕ
hnm : n ≤ m
h : f n x ≤ f m x
⊢ f' n x ≤ f' m x

Tactic:
simp only [f', tsub_le_iff_right, sub_add_cancel]

Premises used: tsub_le_iff_right, sub_add_cancel
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m_1 : 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) ∂μ)
x : α
hx : Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
n m : ℕ
hnm : n ≤ m
⊢ f n x ≤ f m x

Tactic:
hx hnm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m_1 : 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) ∂μ)
x : α
hx : Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
n m : ℕ
hnm : n ≤ m
⊢ f n x ≤ f m x

Tactic:
exact hx hnm
-- 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) ∂μ)
h :
  ∀ (x : α) (hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))),
    Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))

Tactic:
filter_upwards [h_tendsto] with x hx
-- 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) ∂μ)
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))

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 : ∀ (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) ∂μ)
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
h : Tendsto (fun (n : ℕ) ↦ f' n x) atTop (𝓝 ((F - f 0) x))
⊢ Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))

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 : ∀ (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) ∂μ)
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun (n : ℕ) ↦ f' n x) atTop (𝓝 (F x - f 0 x))

Tactic:
Tendsto.sub hx tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- 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) ∂μ)
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun (n : ℕ) ↦ f' n x) atTop (𝓝 (F x - f 0 x))

Tactic:
exact Tendsto.sub hx tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
simpa [neg_neg] using this

Premises used: neg_neg
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
suffices : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
suffices Tendsto (fun n ↦ ∫ x, - -f n x ∂μ) atTop (𝓝 (∫ x, - -F x ∂μ)) by
      simpa [neg_neg] using 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ -∫ (x_1 : α), -f x x_1 ∂μ) atTop (𝓝 (-∫ (x : α), -F x ∂μ))

Tactic:
this.neg

Premises used: Filter.Tendsto.neg
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
h : ∀ (x : ℕ), Eq (α := ℝ) (∫ (x_1 : α), - -f x x_1 ∂μ) (-∫ (x_1 : α), -f x x_1 ∂μ)
h₁ : Eq (α := ℝ) (∫ (x : α), - -F x ∂μ) (-∫ (x : α), -F x ∂μ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))

Tactic:
convert! this.neg

Premises used: Filter.Tendsto.neg
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
x : ℕ
h h₁ : Eq (α := ℝ) (-∫ (a : α), -f x a ∂μ) (-∫ (x_1 : α), -f x x_1 ∂μ)
⊢ Eq (α := ℝ) (∫ (x_1 : α), - -f x x_1 ∂μ) (-∫ (x_1 : α), -f x x_1 ∂μ)

Tactic:
rw [integral_neg]

Premises used: MeasureTheory.integral_neg
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
h h₁ : Eq (α := ℝ) (-∫ (a : α), -F a ∂μ) (-∫ (x : α), -F x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α), - -F x ∂μ) (-∫ (x : α), -F x ∂μ)

Tactic:
rw [integral_neg]

Premises used: MeasureTheory.integral_neg
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
suffices : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
suffices Tendsto (fun n ↦ ∫ x, -f n x ∂μ) atTop (𝓝 (∫ x, -F x ∂μ)) by
    suffices Tendsto (fun n ↦ ∫ x, - -f n x ∂μ) atTop (𝓝 (∫ x, - -F x ∂μ)) by
      simpa [neg_neg] using this
    convert! this.neg <;> rw [integral_neg]
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))

Tactic:
integral_tendsto_of_tendsto_of_monotone (fun n ↦ (hf n).neg) hF.neg ?_ ?_

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.integral_tendsto_of_tendsto_of_monotone
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
refine_1 : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ -f n x
refine_2 : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ -f n x) atTop (𝓝 (-F x))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))

Tactic:
refine integral_tendsto_of_tendsto_of_monotone (fun n ↦ (hf n).neg) hF.neg ?_ ?_

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.integral_tendsto_of_tendsto_of_monotone
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
x : α
hx : Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
n m : ℕ
hnm : n ≤ m
⊢ LE.le (α := ℝ) ((fun (n : ℕ) ↦ -f n x) n) ((fun (n : ℕ) ↦ -f n x) m)

Tactic:
neg_le_neg_iff.mpr <| hx hnm

Premises used: Iff.mpr, neg_le_neg_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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Antitone (β := ℝ) fun (n : ℕ) ↦ f n x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Monotone (β := ℝ) fun (n : ℕ) ↦ -f n x) x} x}
      a
h₁ : ∀ (a : α), (Antitone (β := ℝ) fun (n : ℕ) ↦ f n a) → Monotone (β := ℝ) fun (n : ℕ) ↦ -f n a
h₂ :
  ∀ (x : α) (hx : Antitone (β := ℝ) fun (n : ℕ) ↦ f n x) ⦃n m : ℕ⦄ (hnm : n ≤ m),
    LE.le (α := ℝ) ((fun (n : ℕ) ↦ -f n x) n) ((fun (n : ℕ) ↦ -f n x) m)
⊢ ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ -f n x

Tactic:
filter_upwards [h_mono] with x hx n m hnm using neg_le_neg_iff.mpr <| hx hnm

Premises used: Iff.mpr, neg_le_neg_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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun (n : ℕ) ↦ -f n x) atTop (𝓝 (-F x))

Tactic:
hx.neg

Premises used: Filter.Tendsto.neg
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ -f n x) atTop (𝓝 (-F x))) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))), Tendsto (fun (n : ℕ) ↦ -f n x) atTop (𝓝 (-F x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ -f n x) atTop (𝓝 (-F x))

Tactic:
filter_upwards [h_tendsto] with x hx using hx.neg
-- 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 : ℕ
unfold :
  ∫⁻ (a : α), ENNReal.ofReal (f i a - f 0 a) ∂μ =
    ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
⊢ ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i 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)
i : ℕ
hfi : Integrable (ε := ℝ) (fun (a : α) ↦ f i a - f 0 a) μ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ f i a - f 0 a
⊢ ∫⁻ (a : α), ENNReal.ofReal (f i a - f 0 a) ∂μ =
    ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub (hf_int i) (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)
i : ℕ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ f i a - f 0 a) μ

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

Premises used: MeasureTheory.Integrable.sub, OfNat.ofNat