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 : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
⊢ ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = ∫⁻ (a : α), ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ ∂μ
have e_a : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) fun (a : α) ↦
  ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) fun (a : α) ↦
    ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
have h : ∀ (a : α) (h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0)
  (h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a),
  ENNReal.ofReal (-f a) = ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
Tactic: filter_upwards [Lp.coeFn_negPart f₁, hf.coeFn_toL1] with _ h₁ h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a : α
h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ ENNReal.ofReal (-f a) = ‖(↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a‖ₑ
have h : (↑(-f a).toNNReal : ℝ≥0∞) = ‖-min (f a) 0‖ₑ
Tactic: rw [h₁, h₂, ENNReal.ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a : α
h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ (↑(-f a).toNNReal : ℝ≥0∞) = ‖-min (f a) 0‖ₑ
have h : (-f a).toNNReal = ‖-min (f a) 0‖₊
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a : α
h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ (-f a).toNNReal = ‖-min (f a) 0‖₊
have h : (↑(-f a).toNNReal : ℝ) = (↑‖-min (f a) 0‖₊ : ℝ)
Tactic: apply NNReal.eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a : α
h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ (↑(-f a).toNNReal : ℝ) = (↑‖-min (f a) 0‖₊ : ℝ)
have h : max (-f a) 0 = ‖min (f a) 0‖
Tactic: simp only [Real.coe_toNNReal', coe_nnnorm, nnnorm_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a : α
h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
⊢ max (-f a) 0 = ‖min (f a) 0‖
have h : max (-f a) 0 = -min (f a) 0
Tactic: rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a : α
h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : max (-f a) 0 = -min (f a) 0
⊢ max (-f a) 0 = ‖min (f a) 0‖
have h₃ : max (-f a) 0 = max (-f a) (-0)
Tactic: rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a : α
h₁ : (↑(↑(Lp.negPart f₁) : α →ₘ[μ] ℝ) : α → ℝ) a = -min ((↑(↑f₁ : α →ₘ[μ] ℝ) : α → ℝ) a) 0
h₂ : (↑(↑(Integrable.toL1 f hf) : α →ₘ[μ] ℝ) : α → ℝ) a = f a
h : max (-f a) 0 = -min (f a) 0
h₃ : max (-f a) 0 = max (-f a) (-0)
⊢ max (-f a) 0 = ‖min (f a) 0‖
have h₄ : max (-f a) 0 = max (-f a) 0
Tactic: rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal
have eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖
Tactic: have eq₂ : ENNReal.toReal (∫⁻ a, ENNReal.ofReal (-f a) ∂μ) = ‖Lp.negPart f₁‖ := by
    rw [L1.norm_def]
    congr 1
    apply lintegral_congr_ae
    filter_upwards [Lp.coeFn_negPart f₁, hf.coeFn_toL1] with _ h₁ h₂
    rw [h₁, h₂, ENNReal.ofReal]
    congr 1
    apply NNReal.eq
    simp only [Real.coe_toNNReal', coe_nnnorm, nnnorm_neg]
    rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal
have rw : L1.integral (Integrable.toL1 (fun (a : α) ↦ f a) hf) = ‖Lp.posPart f₁‖ - ‖Lp.negPart f₁‖
Tactic: rw [eq₁, eq₂, integral, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
eq₂ : (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal = ‖Lp.negPart f₁‖
rw : L1.integral (Integrable.toL1 (fun (a : α) ↦ f a) hf) = ‖Lp.posPart f₁‖ - ‖Lp.negPart f₁‖
hc : Integrable (ε := ℝ) (fun (a : α) ↦ f a) μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal
have hc₁ : CompleteSpace ℝ
Tactic: rw [eq₁, eq₂, integral, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have pos : ∀ (hfi : Integrable f μ), ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
pos : ∀ (hfi : Integrable f μ), ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have neg : ∀ (hfi : ¬Integrable f μ), ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have pos : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal =
  (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Tactic: rw [integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0
have rw : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) 0
Tactic: rw [lintegral_eq_zero_iff']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
rw : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) 0
⊢ ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0
have rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) μ
Tactic: rw [lintegral_eq_zero_iff']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) 0
have refine : ∀ (x : α), 0 x ≤ f x → Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ENNReal.ofReal (-f a)) x) (0 x)
Tactic: refine hf.mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have h_min : ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0
Tactic: have h_min : ∫⁻ a, ENNReal.ofReal (-f a) ∂μ = 0 := by
      rw [lintegral_eq_zero_iff']
      · refine hf.mono ?_
        simp only [Pi.zero_apply]
        intro a h
        simp only [h, neg_nonpos, ofReal_eq_zero]
      · exact measurable_ofReal.comp_aemeasurable hfm.aemeasurable.neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
h_min : ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have pos : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - ENNReal.toReal 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Tactic: rw [h_min, toReal_zero, _root_.sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
h_min : ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0
pos : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - ENNReal.toReal 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have pos₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Tactic: rw [h_min, toReal_zero, _root_.sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
h_min : ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0
pos : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - ENNReal.toReal 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
pos₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have pos₂ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Tactic: rw [h_min, toReal_zero, _root_.sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f μ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have neg : 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Tactic: rw [integral_undef hfi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f μ
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have hfi₁ : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
Tactic: simp_rw [Integrable, hfm, hasFiniteIntegral_iff_norm, lt_top_iff_ne_top, Ne, true_and,
      Classical.not_not] at hfi
Cleared hypotheses: hfi
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
have refine : ∀ (a : α) (h : 0 a ≤ f a),
  Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ENNReal.ofReal (f a)) a) ((fun (a : α) ↦ ENNReal.ofReal ‖f a‖) a)
Tactic: refine lintegral_congr_ae (hf.mono fun a h => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal ‖f a‖
have rw : ENNReal.ofReal (f a) = ENNReal.ofReal |f a|
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
a : α
h : 0 a ≤ f a
rw : ENNReal.ofReal (f a) = ENNReal.ofReal |f a|
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal ‖f a‖
have rw₁ : ENNReal.ofReal (f a) = ENNReal.ofReal (f a)
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have this : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
Tactic: have : ∫⁻ a : α, ENNReal.ofReal (f a) ∂μ = ∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ := by
      refine lintegral_congr_ae (hf.mono fun a h => ?_)
      dsimp only
      rw [Real.norm_eq_abs, abs_of_nonneg h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
this : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have neg : 0 = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
Tactic: rw [this, hfi, toReal_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
this : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
neg : 0 = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have neg₁ : 0 = ENNReal.toReal ∞
Tactic: rw [this, hfi, toReal_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
this : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
neg : 0 = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal
neg₁ : 0 = ENNReal.toReal ∞
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
have neg₂ : Eq (α := ℝ) 0 0
Tactic: rw [this, hfi, toReal_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : α), ‖f x‖ ∂μ = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal
have rw : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae _ hf.norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
rw : (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal
⊢ ∫ (x : α), ‖f x‖ ∂μ = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal
have rw₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖f x‖
Tactic: rw [integral_eq_lintegral_of_nonneg_ae _ hf.norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖f x‖
have h : ∀ (a : α), 0 a ≤ ‖f a‖
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ ∀ (a : α), 0 a ≤ ‖f a‖
have h : ∀ (a : α), 0 ≤ ‖f a‖
Tactic: simp_rw [Pi.zero_apply, norm_nonneg, imp_true_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
h : ∀ (a : α), 0 ≤ ‖f a‖
⊢ ∀ (a : α), 0 a ≤ ‖f a‖
have h₁ : ∀ (a : α), True
Tactic: simp_rw [Pi.zero_apply, norm_nonneg, imp_true_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : Integrable f μ
⊢ ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ
have rw : ∫⁻ (x : α), ‖f x‖ₑ ∂μ ≠ ∞
Tactic: rw [integral_norm_eq_lintegral_enorm hf.aestronglyMeasurable, ENNReal.ofReal_toReal]
-- 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 α
inst_2 : CompleteSpace E
f : α →ₛ E
hfi : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ integral μ f = ∫ (x : α), (f : (a : α) → E) x ∂μ
have rw : integral μ f = integral μ (Lp.simpleFunc.toSimpleFunc (f.toLp sorry))
Tactic: rw [MeasureTheory.integral_eq f hfi, ← L1.SimpleFunc.toLp_one_eq_toL1,
    L1.SimpleFunc.integral_L1_eq_integral, L1.SimpleFunc.integral_eq_integral]
-- 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 α
inst_2 : CompleteSpace E
f : α →ₛ E
hfi : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ Eq (α := E) (∫ (x : α), (f : (a : α) → E) x ∂μ) (∑ x ∈ f.range, μ.real (preimage (β := E) (⇑f : (a : α) → E) {x}) • x)
have rw : setToSimpleFunc (weightedSMul μ) f = integral μ f
Tactic: rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → E
s : Set E
inst_5 : SeparableSpace.{u_2} (↑s : Type u_2)
hfi : Integrable f μ
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ y₀) μ
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop
    (𝓝 (∫ (x : α), f x ∂μ))
have hfi' : ∀ (n : ℕ), Integrable.{u_2, u_1} (ε := E) (⇑(approxOn f hfm s y₀ h₀ n) : (a : α) → E) μ
Tactic: have hfi' := SimpleFunc.integrable_approxOn hfm hfi h₀ h₀i
-- 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 α
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → E
s : Set E
inst_5 : SeparableSpace.{u_2} (↑s : Type u_2)
hfi : Integrable f μ
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ y₀) μ
hfi' : ∀ (n : ℕ), Integrable.{u_2, u_1} (ε := E) (⇑(approxOn f hfm s y₀ h₀ n) : (a : α) → E) μ
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop
    (𝓝 (∫ (x : α), f x ∂μ))
have simp : Tendsto.{0, u_2} (β := E)
  (fun (n : ℕ) ↦
    if x : CompleteSpace E then
      if hf : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (approxOn f hfm s y₀ h₀ n : (a : α) → E) x) μ then
        (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E)
          (Integrable.toL1 (fun (x : α) ↦ (approxOn f hfm s y₀ h₀ n : (a : α) → E) x) hf)
      else 0
    else 0)
  atTop
  (𝓝
    (if x : CompleteSpace E then
      if hf : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x) μ then
        (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E) (Integrable.toL1 (fun (x : α) ↦ f x) hf)
      else 0
    else 0))
Tactic: simp only [SimpleFunc.integral_eq_integral _ (hfi' _), integral, L1.integral]
-- 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 α
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst_5 : SeparableSpace.{u_2} (↑s : Type u_2)
hs : range f ∪ {0} ⊆ s
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn f fmeas s 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), f x ∂μ))
have apply : ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Tactic: apply tendsto_integral_approxOn_of_measurable hf fmeas _ _ (integrable_zero _ _ _)