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_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) atTop (𝓝 (F a))
have h₁ : Tendsto (fun (i : ℕ) ↦ (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))
Tactic: rw [h1, h2]
-- 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 ∂μ))
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))
have h₁ : Tendsto (fun (i : ℕ) ↦ (f' i a).toReal) atTop (𝓝 (F' a).toReal)
Tactic: refine Filter.Tendsto.add ?_ tendsto_const_nhds
-- 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 : α) ∂μ, 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 : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h : ∀ (a : α) (ha_tendsto : Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
Tactic: filter_upwards [this] with a ha_tendsto
-- 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 : α) ∂μ, 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 (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h : ∀ (x : ℕ), f x a = -f' x a
Tactic: convert! ha_tendsto.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 : α) ∂μ, 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
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
have h₁ : F a = -F' a
Tactic: convert! ha_tendsto.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 : α) ∂μ, 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))
have suffices : ∀ᵐ (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']
-- 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 : α) ∂μ, 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))
have refine_1 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f' i a ∂μ) atTop (𝓝 (∫ (a : α), F' a ∂μ))
Tactic: refine tendsto_of_integral_tendsto_of_monotone (fun n ↦ (hf_int n).neg) hF_int.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 : α) ∂μ, 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 ∂μ))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
have refine_2 : ∀ᵐ (a : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f' i a
Tactic: refine tendsto_of_integral_tendsto_of_monotone (fun n ↦ (hf_int n).neg) hF_int.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 : α) ∂μ, 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
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f' i a) atTop (𝓝 (F' a))
have refine_3 : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
Tactic: refine tendsto_of_integral_tendsto_of_monotone (fun n ↦ (hf_int n).neg) hF_int.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 : α) ∂μ, 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 (i : ℕ) ↦ ∫ (a : α), f' i a ∂μ) atTop (𝓝 (∫ (a : α), F' a ∂μ))
have h : ∀ (x : ℕ), Eq (α := ℝ) (∫ (a : α), f' x a ∂μ) (-∫ (a : α), f x a ∂μ)
Tactic: convert! hf_tendsto.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 : α) ∂μ, 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 ∂μ)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (a : α), f' i a ∂μ) atTop (𝓝 (∫ (a : α), F' a ∂μ))
have h₁ : Eq (α := ℝ) (∫ (a : α), F' a ∂μ) (-∫ (a : α), F a ∂μ)
Tactic: convert! hf_tendsto.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 : α) ∂μ, 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 : ℕ
⊢ Eq (α := ℝ) (∫ (a : α), f' x a ∂μ) (-∫ (a : α), f x a ∂μ)
have h : Eq (α := ℝ) (-∫ (a : α), f x a ∂μ) (-∫ (a : α), f x a ∂μ)
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_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
⊢ Eq (α := ℝ) (∫ (a : α), F' a ∂μ) (-∫ (a : α), F a ∂μ)
have h : Eq (α := ℝ) (-∫ (a : α), F a ∂μ) (-∫ (a : α), F a ∂μ)
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_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 : α) ∂μ, Monotone (β := ℝ) fun (i : ℕ) ↦ f' i a
have 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)
Tactic: filter_upwards [hf_mono] with a ha i j hij
-- 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 : α) ∂μ, 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 : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
have h : ∀ (a : α) (ha : ∀ (i : ℕ), F a ≤ f i a) (i : ℕ), f' i a ≤ F' a
Tactic: filter_upwards [hf_bound] with a ha i
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : ↥(Lp H 1 μ)
⊢ ‖f‖ = ∫ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ ∂μ
have simp : (∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ₑ ∂μ).toReal = ∫ (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
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 : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ ∂μ
have rw : (∫⁻ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ₑ ∂μ).toReal =
  (∫⁻ (a : α), ENNReal.ofReal ‖(↑(↑f : α →ₘ[μ] H) : α → H) a‖ ∂μ).toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall (by simp [norm_nonneg]))
      (Lp.aestronglyMeasurable f).norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f g : ↥(Lp H 1 μ)
⊢ dist f g = ∫ (a : α), dist ((↑(↑f : α →ₘ[μ] H) : α → H) a) ((↑(↑g : α →ₘ[μ] H) : α → H) a) ∂μ
have simp : Eq (α := ℝ) (∫ (a : α), ‖(↑(↑(f - g) : α →ₘ[μ] H) : α → H) a‖ ∂μ)
  (∫ (a : α), ‖(↑(↑f : α →ₘ[μ] H) : α → H) a - (↑(↑g : α →ₘ[μ] H) : α → H) a‖ ∂μ)
Tactic: simp only [dist_eq_norm, L1.norm_eq_integral_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ = ∫ (a : α), ‖f a‖ ∂μ
have rw : Eq (α := ℝ) (∫ (a : α), ‖(↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] H) : α → H) a‖ ∂μ) (∫ (a : α), ‖f a‖ ∂μ)
Tactic: rw [L1.norm_eq_integral_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
have simp_rw : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
Tactic: simp_rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
⊢ eLpNorm f p μ = ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)
have A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
Tactic: have A : ∫⁻ a : α, ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ a : α, ‖f a‖ₑ ^ p.toReal ∂μ := by
    simp_rw [← ofReal_rpow_of_nonneg (norm_nonneg _) toReal_nonneg, ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ eLpNorm f p μ = ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)
have simp : (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
  ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)
Tactic: simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal hp1 hp2, one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)
have rw : (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
  ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)
Tactic: rw [integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
rw :
  (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)
have hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p.toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
rw :
  (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)
hf₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖f a‖ ^ p.toReal
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal (HPow.hPow (α := ℝ) (∫ (a : α), ‖f a‖ ^ p.toReal ∂μ) p.toReal⁻¹)
have hfm : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ ‖f a‖ ^ p.toReal) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ).toReal ^ p.toReal⁻¹)
have rw : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞
Tactic: rw [A, ← ofReal_rpow_of_nonneg toReal_nonneg (inv_nonneg.2 toReal_nonneg), ofReal_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
have le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
Tactic: have le_ae : ∀ᵐ a ∂μ, 0 ≤ ‖f a‖ := Eventually.of_forall fun a => norm_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
have pos : ∀ (h : AEStronglyMeasurable f μ), norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
Tactic: by_cases h : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
pos : ∀ (h : AEStronglyMeasurable f μ), norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
have neg : ∀ (h : ¬AEStronglyMeasurable f μ), norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
Tactic: by_cases h : AEStronglyMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ
⊢ norm.{u_5} (E := G) (∫ (a : α), f a ∂μ) ≤ ∫ (a : α), ‖f a‖ ∂μ
have neg : LE.le (α := ℝ) 0 (∫ (a : α), ‖f a‖ ∂μ)
Tactic: rw [integral_non_aestronglyMeasurable h, norm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
⊢ ∫ (x : α), c ∂μ = μ.real univ • c
have pos : ∀ (hμ : IsFiniteMeasure μ), ∫ (x : α), c ∂μ = μ.real univ • c
Tactic: by_cases hμ : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
pos : ∀ (hμ : IsFiniteMeasure μ), ∫ (x : α), c ∂μ = μ.real univ • c
⊢ ∫ (x : α), c ∂μ = μ.real univ • c
have neg : ∀ (hμ : ¬IsFiniteMeasure μ), ∫ (x : α), c ∂μ = μ.real univ • c
Tactic: by_cases hμ : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : IsFiniteMeasure μ
⊢ ∫ (x : α), c ∂μ = μ.real univ • c
have pos : (setToFun μ (weightedSMul μ) sorry fun (a : α) ↦ c) = μ.real univ • c
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
⊢ ∫ (x : α), c ∂μ = μ.real univ • c
have pos : ∀ (hc : c = 0), ∫ (x : α), c ∂μ = μ.real univ • c
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
c : E
hμ : ¬IsFiniteMeasure μ
pos : ∀ (hc : c = 0), ∫ (x : α), c ∂μ = μ.real univ • c
⊢ ∫ (x : α), c ∂μ = μ.real univ • c
have neg : ∀ (hc : ¬c = 0), ∫ (x : α), c ∂μ = μ.real univ • c
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst_2 : IsFiniteMeasure μ
f : α → G
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ ∫ (x : α), C ∂μ = C * μ.real univ
have rw : μ.real univ • C = C * μ.real univ
Tactic: rw [integral_const, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst_2 : IsFiniteMeasure μ
f : α → G
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
rw : μ.real univ • C = C * μ.real univ
⊢ ∫ (x : α), C ∂μ = C * μ.real univ
have rw₁ : μ.real univ * C = C * μ.real univ
Tactic: rw [integral_const, smul_eq_mul, mul_comm]