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)
hf'_int_eq :
  ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
h_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ≥0∞) fun (i : ℕ) ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
⊢ F a = (F' a).toReal + f 0 a

Tactic:
have h2 : F a = (F' a).toReal + f 0 a := by
    unfold F'
    rw [ENNReal.toReal_ofReal]
    · abel
    · simp [ha_bound 0]
-- 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_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
h₁ : Tendsto (fun (i : ℕ) ↦ (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))

Tactic:
rw [h1, h2]
-- 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_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ Tendsto (fun (i : ℕ) ↦ (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))

Tactic:
Filter.Tendsto.add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- 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_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
h₁ : Tendsto (fun (i : ℕ) ↦ (f' i a).toReal) atTop (𝓝 (F' a).toReal)
⊢ Tendsto (fun (i : ℕ) ↦ (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))

Tactic:
refine Filter.Tendsto.add ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- 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_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ F' a ≠ ∞

Tactic:
finiteness
-- 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_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : Eq (α := (i : ℕ) → ℝ) (fun (i : ℕ) ↦ f i a) fun (i : ℕ) ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ Tendsto (fun (i : ℕ) ↦ (f' i a).toReal) atTop (𝓝 (F' a).toReal)

Tactic:
exact (ENNReal.continuousAt_toReal (by finiteness)).tendsto.comp ha

Premises used: ENNReal.continuousAt_toReal, ContinuousAt.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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
h :
  ∀ (a : α) (ha_tendsto : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))),
    Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))

Tactic:
filter_upwards [this] with a ha_tendsto
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha_tendsto : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
⊢ Tendsto (fun (x : ℕ) ↦ -f' x a) atTop (𝓝 (-F' a))

Tactic:
ha_tendsto.neg

Premises used: Filter.Tendsto.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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha_tendsto : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
h : ∀ (x : ℕ), f x a = -f' x a
h₁ : F a = -F' a
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))

Tactic:
convert! ha_tendsto.neg

Premises used: Filter.Tendsto.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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha_tendsto : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
x : ℕ
⊢ f x a = -f' x a

Tactic:
simp [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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha_tendsto : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
⊢ F a = -F' a

Tactic:
simp [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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
suffices : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))

Tactic:
suffices ∀ᵐ a ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a)) by
    filter_upwards [this] with a ha_tendsto
    convert! ha_tendsto.neg
    · simp [f']
    · simp [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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))

Tactic:
tendsto_of_integral_tendsto_of_monotone (fun n ↦ (hf_int n).neg) hF_int.neg ?_ ?_ ?_

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.tendsto_of_integral_tendsto_of_monotone
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
refine_1 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f' i a ∂μ) atTop (𝓝 (∫ (a : α), F' a ∂μ))
refine_2 : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f' i a
refine_3 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))

Tactic:
refine tendsto_of_integral_tendsto_of_monotone (fun n ↦ (hf_int n).neg) hF_int.neg ?_ ?_ ?_

Premises used: MeasureTheory.Integrable.neg, MeasureTheory.tendsto_of_integral_tendsto_of_monotone
-- 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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ -∫ (a : α), f x a ∂μ) atTop (𝓝 (-∫ (a : α), F a ∂μ))

Tactic:
hf_tendsto.neg

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

Tactic:
convert! hf_tendsto.neg

Premises used: Filter.Tendsto.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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
x : ℕ
h h₁ : Eq (α := ℝ) (-∫ (a : α), f x a ∂μ) (-∫ (a : α), f x a ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), f' x a ∂μ) (-∫ (a : α), f x a ∂μ)

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_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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
h h₁ : Eq (α := ℝ) (-∫ (a : α), F a ∂μ) (-∫ (a : α), F a ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), F' a ∂μ) (-∫ (a : α), F a ∂μ)

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_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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
h :
  ∀ (a : α) (ha : Antitone (β := ℝ) fun (i : ℕ) ↦ f i a) ⦃i j : ℕ⦄ (hij : i ≤ j),
    LE.le (α := ℝ) ((fun (i : ℕ) ↦ f' i a) i) ((fun (i : ℕ) ↦ f' i a) j)
⊢ ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f' i a

Tactic:
filter_upwards [hf_mono] with a ha 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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
a : α
ha : Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
i j : ℕ
hij : i ≤ j
⊢ LE.le (α := ℝ) ((fun (i : ℕ) ↦ f' i a) i) ((fun (i : ℕ) ↦ f' i a) j)

Tactic:
simp [f', ha 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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
h : ∀ (a : α) (ha : ∀ (i : ℕ), F a ≤ f i a) (i : ℕ), f' i a ≤ F' a
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a

Tactic:
filter_upwards [hf_bound] with a ha 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 : α) ∂μ, Antitone (β := ℝ) fun (i : ℕ) ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun (i : ℕ) (a : α) ↦ -f i a
F' : α → ℝ := fun (a : α) ↦ -F a
a : α
ha : ∀ (i : ℕ), F a ≤ f i a
i : ℕ
⊢ f' i a ≤ F' a

Tactic:
simp [f', F', ha i]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
simp : (∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ₑ ∂μ).toReal = ∫ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ ∂μ
⊢ ‖f‖ = ∫ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ ∂μ

Tactic:
simp only [eLpNorm, eLpNorm'_eq_lintegral_enorm, ENNReal.toReal_one, ENNReal.rpow_one,
    Lp.norm_def, if_false, ENNReal.one_ne_top, one_ne_zero, _root_.div_one]

Premises used: ENNReal.toReal_one, ENNReal.rpow_one, if_false, MeasureTheory.eLpNorm'_eq_lintegral_enorm, one_ne_zero, div_one, ENNReal.one_ne_top, MeasureTheory.eLpNorm, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ ∀ (x : α), 0 x ≤ ‖(↑(↑f : α →ₘ[μ] H) : α → H) x‖

Tactic:
simp [norm_nonneg]

Premises used: norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
rw :
  (∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ ∂μ).toReal
⊢ (∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ₑ ∂μ).toReal = ∫ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall (by simp [norm_nonneg]))
      (Lp.aestronglyMeasurable f).norm]

Premises used: MeasureTheory.Lp.aestronglyMeasurable, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ (∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ ∂μ).toReal

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f g : ↥(Lp H 1 μ)
simp :
  Eq (α := ℝ) (∫ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] H) : α → H) a‖ ∂μ)
    (∫ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a - (↑(↑g : α →ₘ[μ] H) : α → H) a‖ ∂μ)
⊢ dist f g = ∫ (a : α), dist ((↑(↑f : α →ₘ[μ] H) : α → H) a) ((↑(↑g : α →ₘ[μ] H) : α → H) a) ∂μ

Tactic:
simp only [dist_eq_norm, L1.norm_eq_integral_norm]

Premises used: dist_eq_norm, MeasureTheory.L1.norm_eq_integral_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f g : ↥(Lp H 1 μ)
⊢ Eq (α := ℝ) (∫ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] H) : α → H) a‖ ∂μ)
    (∫ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a - (↑(↑g : α →ₘ[μ] H) : α → H) a‖ ∂μ)

Tactic:
integral_congr_ae <| (Lp.coeFn_sub _ _).fun_comp norm

Premises used: Norm.norm, MeasureTheory.integral_congr_ae, MeasureTheory.Lp.coeFn_sub, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f g : ↥(Lp H 1 μ)
⊢ Eq (α := ℝ) (∫ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] H) : α → H) a‖ ∂μ)
    (∫ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a - (↑(↑g : α →ₘ[μ] H) : α → H) a‖ ∂μ)

Tactic:
exact integral_congr_ae <| (Lp.coeFn_sub _ _).fun_comp norm

Premises used: Norm.norm, MeasureTheory.integral_congr_ae, MeasureTheory.Lp.coeFn_sub, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
rw : Eq (α := ℝ) (∫ (a : α), ‖(↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] H) : α → H) a‖ ∂μ) (∫ (a : α), ‖f a‖ ∂μ)
⊢ ‖Integrable.toL1 f hf‖ = ∫ (a : α), ‖f a‖ ∂μ

Tactic:
rw [L1.norm_eq_integral_norm]

Premises used: MeasureTheory.L1.norm_eq_integral_norm