awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 : (-f a).toNNReal = ‖-min (f a) 0‖₊
⊢ (↑(-f a).toNNReal : ℝ≥0∞) = ‖-min (f a) 0‖ₑ

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 : (↑(-f a).toNNReal : ℝ) = (↑‖-min (f a) 0‖₊ : ℝ)
⊢ (-f a).toNNReal = ‖-min (f a) 0‖₊

Tactic:
apply NNReal.eq

Premises used: NNReal.eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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‖
⊢ (↑(-f a).toNNReal : ℝ) = (↑‖-min (f a) 0‖₊ : ℝ)

Tactic:
simp only [Real.coe_toNNReal', coe_nnnorm, nnnorm_neg]

Premises used: Real.coe_toNNReal', nnnorm_neg, coe_nnnorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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)
h₄ h₅ : max (-f a) 0 = max (-f a) 0
⊢ max (-f a) 0 = ‖min (f a) 0‖

Tactic:
rw [Real.norm_of_nonpos (min_le_right _ _), ← max_neg_neg, neg_zero]

Premises used: max_neg_neg, Real.norm_of_nonpos, min_le_right, neg_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) ∂μ).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]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
hc₁ : CompleteSpace ℝ
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal

Tactic:
rw [eq₁, eq₂, integral, dif_pos, dif_pos]

Premises used: dif_pos, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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₁‖
⊢ L1.integral (Integrable.toL1 (fun (a : α) ↦ f a) hf) = ‖Lp.posPart f₁‖ - ‖Lp.negPart f₁‖

Tactic:
L1.integral_eq_norm_posPart_sub _

Premises used: MeasureTheory.L1.integral_eq_norm_posPart_sub
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
neg : ∀ (hfi : ¬Integrable f μ), ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
by_cases hfi : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
pos :
  (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
rw [integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi]

Premises used: MeasureTheory.integral_eq_lintegral_pos_part_sub_lintegral_neg_part
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ = 0

Tactic:
rw [lintegral_eq_zero_iff']

Premises used: MeasureTheory.lintegral_eq_zero_iff'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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

Tactic:
hf.mono ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
refine : ∀ (x : α), 0 x ≤ f x → Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ENNReal.ofReal (-f a)) x) (0 x)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) 0

Tactic:
refine hf.mono ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
a : α
h : 0 ≤ f a
⊢ ENNReal.ofReal (-f a) = 0

Tactic:
simp only [h, neg_nonpos, ofReal_eq_zero]

Premises used: ENNReal.ofReal_eq_zero, neg_nonpos
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) μ

Tactic:
measurable_ofReal.comp_aemeasurable hfm.aemeasurable.neg

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, ENNReal.ofNNReal, ENNReal.ofReal, AEMeasurable.neg, WithTop.some, ENNReal.measurable_ofReal, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (-f a)) μ

Tactic:
exact measurable_ofReal.comp_aemeasurable hfm.aemeasurable.neg

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.neg, ENNReal.measurable_ofReal, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ∫⁻ (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
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
pos₂ pos₃ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
rw [h_min, toReal_zero, _root_.sub_zero]

Premises used: sub_zero, ENNReal.toReal_zero
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f μ
neg : 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
⊢ ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
rw [integral_undef hfi]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬Integrable f μ
⊢ ∫⁻ (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

Premises used: Classical.not_not, MeasureTheory.Integrable, Ne, lt_top_iff_ne_top, MeasureTheory.hasFiniteIntegral_iff_norm, true_and
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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‖ ∂μ

Tactic:
lintegral_congr_ae (hf.mono fun a h => ?_)

Premises used: MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
refine :
  ∀ (a : α) (h : 0 a ≤ f a),
    Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ENNReal.ofReal (f a)) a) ((fun (a : α) ↦ ENNReal.ofReal ‖f a‖) a)
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ

Tactic:
refine lintegral_congr_ae (hf.mono fun a h => ?_)

Premises used: MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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|
rw₁ rw₂ : ENNReal.ofReal (f a) = ENNReal.ofReal (f a)
⊢ ENNReal.ofReal (f a) = ENNReal.ofReal ‖f a‖

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg h]

Premises used: abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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‖ ∂μ

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]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∞
neg₂ neg₃ : Eq (α := ℝ) 0 0
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
rw [this, hfi, toReal_top]

Premises used: ENNReal.toReal_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
rw₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖f x‖
⊢ ∫ (x : α), ‖f x‖ ∂μ = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae _ hf.norm]

Premises used: MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

Tactic:
simp_rw [ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
h : ∀ (a : α), 0 a ≤ ‖f a‖
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖f x‖

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
h : ∀ (a : α), 0 ≤ ‖f a‖
h₁ : ∀ (a : α), True
⊢ ∀ (a : α), 0 a ≤ ‖f a‖

Tactic:
simp_rw [Pi.zero_apply, norm_nonneg, imp_true_iff]

Premises used: Pi.zero_apply, imp_true_iff, norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : Integrable f μ
rw : ∫⁻ (x : α), ‖f x‖ₑ ∂μ ≠ ∞
⊢ ENNReal.ofReal (∫ (x : α), ‖f x‖ ∂μ) = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

Tactic:
rw [integral_norm_eq_lintegral_enorm hf.aestronglyMeasurable, ENNReal.ofReal_toReal]

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.integral_norm_eq_lintegral_enorm, ENNReal.ofReal_toReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : Integrable f μ
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ ≠ ∞

Tactic:
lt_top_iff_ne_top.mp (hasFiniteIntegral_iff_enorm.mpr hf.2)

Premises used: Iff.mpr, lt_top_iff_ne_top, And.right, Iff.mp, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst : NormedAddCommGroup P
f : α → P
hf : Integrable f μ
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ ≠ ∞

Tactic:
exact lt_top_iff_ne_top.mp (hasFiniteIntegral_iff_enorm.mpr hf.2)

Premises used: Iff.mpr, lt_top_iff_ne_top, And.right, Iff.mp, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
rw : integral μ f = integral μ (Lp.simpleFunc.toSimpleFunc (f.toLp ⋯))
⊢ integral μ f = ∫ (x : α), (f : (a : α) → E) x ∂μ

Tactic:
rw [MeasureTheory.integral_eq f hfi, ← L1.SimpleFunc.toLp_one_eq_toL1,
    L1.SimpleFunc.integral_L1_eq_integral, L1.SimpleFunc.integral_eq_integral]

Premises used: MeasureTheory.L1.SimpleFunc.toLp_one_eq_toL1, MeasureTheory.integral_eq, MeasureTheory.L1.SimpleFunc.integral_L1_eq_integral, DFunLike.coe, MeasureTheory.L1.SimpleFunc.integral_eq_integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 = integral μ (Lp.simpleFunc.toSimpleFunc (f.toLp ⋯))

Tactic:
SimpleFunc.integral_congr hfi (Lp.simpleFunc.toSimpleFunc_toLp _ _).symm

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp, MeasureTheory.SimpleFunc.integral_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 = integral μ (Lp.simpleFunc.toSimpleFunc (f.toLp ⋯))

Tactic:
exact SimpleFunc.integral_congr hfi (Lp.simpleFunc.toSimpleFunc_toLp _ _).symm

Premises used: MeasureTheory.Lp.simpleFunc.toSimpleFunc_toLp, MeasureTheory.SimpleFunc.integral_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
rw : setToSimpleFunc (weightedSMul μ) f = integral μ f
⊢ Eq (α := E) (∫ (x : α), (f : (a : α) → E) x ∂μ) (∑ x ∈ f.range, μ.real (preimage (β := E) (⇑f : (a : α) → E) {x}) • x)

Tactic:
rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]

Premises used: MeasureTheory.SimpleFunc.integral_eq_integral, MeasureTheory.SimpleFunc.integral, MeasureTheory.SimpleFunc.integral_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
⊢ setToSimpleFunc (weightedSMul μ) f = integral μ f

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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₀) μ
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) μ
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))
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop
    (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
simp only [SimpleFunc.integral_eq_integral _ (hfi' _), integral, L1.integral]

Premises used: MeasureTheory.SimpleFunc.integral_eq_integral, MeasureTheory.integral, MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 : ℕ) ↦
      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:
tendsto_setToFun_approxOn_of_measurable (dominatedFinMeasAdditive_weightedSMul μ)
    hfi hfm hs h₀ h₀i

Premises used: Set.Mem, MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.SimpleFunc.integral, MeasureTheory.tendsto_setToFun_approxOn_of_measurable, MeasureTheory.L1.SimpleFunc.integralCLM', MeasureTheory.dominatedFinMeasAdditive_weightedSMul, MeasureTheory.setToFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 : ℕ) ↦
      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:
exact tendsto_setToFun_approxOn_of_measurable (dominatedFinMeasAdditive_weightedSMul μ)
    hfi hfm hs h₀ h₀i

Premises used: MeasureTheory.tendsto_setToFun_approxOn_of_measurable, MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedDivisionRing 𝕜
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
G : Type u_5
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace ℝ E
f_1 : α → E
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst_8 : TopologicalSpace X
inst_9 : FirstCountableTopology X
inst_10 : CompleteSpace E
inst_11 : MeasurableSpace E
inst_12 : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst_13 : SeparableSpace.{u_2} (↑s : Type u_2)
hs : range f ∪ {0} ⊆ s
n : ℕ
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp