awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
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 : α) ∂μ, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)
have 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)
Tactic: filter_upwards [h_mono] with x hx n m hnm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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)
have h : f' n x ≤ f' m x
Tactic: refine ENNReal.ofReal_le_ofReal ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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
have h : f n x ≤ f m x
Tactic: simp only [f', tsub_le_iff_right, sub_add_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))
have 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)))
Tactic: filter_upwards [h_tendsto] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
f' : (n : ℕ) → (x : α) → ℝ := fun (n : ℕ) (x : α) ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
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)))
have h : Tendsto (fun (n : ℕ) ↦ f' n x) atTop (𝓝 ((F - f 0) x))
Tactic: refine (ENNReal.continuous_ofReal.tendsto _).comp ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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 (n : ℕ) ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))
have suffices : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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 (n : ℕ) ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))
have h : ∀ (x : ℕ), Eq (α := ℝ) (∫ (x_1 : α), - -f x x_1 ∂μ) (-∫ (x_1 : α), -f x x_1 ∂μ)
Tactic: convert! this.neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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 ∂μ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), - -f n x ∂μ) atTop (𝓝 (∫ (x : α), - -F x ∂μ))
have h₁ : Eq (α := ℝ) (∫ (x : α), - -F x ∂μ) (-∫ (x : α), -F x ∂μ)
Tactic: convert! this.neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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 : ℕ
⊢ Eq (α := ℝ) (∫ (x_1 : α), - -f x x_1 ∂μ) (-∫ (x_1 : α), -f x x_1 ∂μ)
have h : Eq (α := ℝ) (-∫ (a : α), -f x a ∂μ) (-∫ (x_1 : α), -f x x_1 ∂μ)
Tactic: rw [integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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 ∂μ))
⊢ Eq (α := ℝ) (∫ (x : α), - -F x ∂μ) (-∫ (x : α), -F x ∂μ)
have h : Eq (α := ℝ) (-∫ (a : α), -F a ∂μ) (-∫ (x : α), -F x ∂μ)
Tactic: rw [integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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 ∂μ))
have suffices : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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 ∂μ))
have refine_1 : ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ -f n x
Tactic: refine integral_tendsto_of_tendsto_of_monotone (fun n ↦ (hf n).neg) hF.neg ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
have refine_2 : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ -f n x) atTop (𝓝 (-F x))
Tactic: refine integral_tendsto_of_tendsto_of_monotone (fun n ↦ (hf n).neg) hF.neg ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ -f n x
have 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
Tactic: filter_upwards [h_mono] with x hx n m hnm using neg_le_neg_iff.mpr <| hx hnm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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
⊢ ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ -f n x
have h₁ : ∀ (a : α), (Antitone (β := ℝ) fun (n : ℕ) ↦ f n a) → Monotone (β := ℝ) fun (n : ℕ) ↦ -f n a
Tactic: filter_upwards [h_mono] with x hx n m hnm using neg_le_neg_iff.mpr <| hx hnm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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
⊢ ∀ᵐ (x : α) ∂μ, Monotone (β := ℝ) fun (n : ℕ) ↦ -f n x
have 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)
Tactic: filter_upwards [h_mono] with x hx n m hnm using neg_le_neg_iff.mpr <| hx hnm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone (β := ℝ) fun (n : ℕ) ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (F x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ -f n x) atTop (𝓝 (-F x))
have 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
Tactic: filter_upwards [h_tendsto] with x hx using hx.neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, 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
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ -f n x) atTop (𝓝 (-F x))
have h₁ : ∀ (a : α), Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (F a)) → Tendsto (fun (n : ℕ) ↦ -f n a) atTop (𝓝 (-F a))
Tactic: filter_upwards [h_tendsto] with x hx using hx.neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : α), ENNReal.ofReal (f i a - f 0 a) ∂μ =
    ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
have hfi : Integrable (ε := ℝ) (fun (a : α) ↦ f i a - f 0 a) μ
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub (hf_int i) (hf_int 0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (f i a - f 0 a) ∂μ =
    ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ))
have f_nn : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ f i a - f 0 a
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub (hf_int i) (hf_int 0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : ℕ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ f i a - f 0 a
have h : ∀ (a : α) (h_mono : Monotone (β := ℝ) fun (i : ℕ) ↦ f i a), 0 a ≤ f i a - f 0 a
Tactic: filter_upwards [hf_mono] with a h_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have hf'_int_eq : ∀ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : α), ENNReal.ofReal (F a - f 0 a) ∂μ =
    ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
have hfi : Integrable (ε := ℝ) (fun (a : α) ↦ F a - f 0 a) μ
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub hF_int (hf_int 0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (F a - f 0 a) ∂μ =
    ENNReal.ofReal (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ))
have f_nn : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ F a - f 0 a
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal, integral_sub hF_int (hf_int 0)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 ∂μ))
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ F a - f 0 a
have h : ∀ (a : α) (h_bound : ∀ (i : ℕ), f i a ≤ F a), 0 a ≤ F a - f 0 a
Tactic: filter_upwards [hf_bound] with a h_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
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 : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have hF'_int_eq : ∫⁻ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 ∂μ))
have 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 ∂μ))))
Tactic: simp_rw [hf'_int_eq, hF'_int_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 ∂μ))))
have refine : Tendsto (fun (i : ℕ) ↦ HSub.hSub (α := ℝ) (∫ (a : α), f i a ∂μ) (∫ (a : α), f 0 a ∂μ)) atTop
  (𝓝 (HSub.hSub (α := ℝ) (∫ (a : α), F a ∂μ) (∫ (a : α), f 0 a ∂μ)))
Tactic: refine (ENNReal.continuous_ofReal.tendsto _).comp ?_