-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_eq_lintegral_pos_part_sub_lintegral_neg_part {f : α → ℝ} (hf : Integrable f μ) :
    ∫ a, f a ∂μ =
      ENNReal.toReal (∫⁻ a, .ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ a, .ofReal (-f a) ∂μ)

Proof state:
α : 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

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]

Result:
α : 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

Proof state:
α : 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) ?hc) = ‖Lp.posPart f₁‖ - ‖Lp.negPart f₁‖

case hc
α : 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₁‖
⊢ Integrable (fun a => f a) μ

case hc
α : 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₁‖
⊢ CompleteSpace ℝ

Tactic:
exact L1.integral_eq_norm_posPart_sub _

Result:
no goals

Proof state:
case h.e_a
α : 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✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ (-f a✝).toNNReal = ‖-(f a✝ ⊓ 0)‖₊

Tactic:
apply NNReal.eq

Result:
case h.e_a.a
α : 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✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(-f a✝).toNNReal = ↑‖-(f a✝ ⊓ 0)‖₊

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖

Tactic:
rw [L1.norm_def]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = (∫⁻ (a : α), ‖↑↑(Lp.posPart f₁) a‖ₑ ∂μ).toReal

Proof state:
case h
α : 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✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ‖↑↑(Lp.negPart f₁) a✝‖ₑ

Tactic:
rw [h₁, h₂, ENNReal.ofReal]

Result:
case h
α : 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✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(-f a✝).toNNReal = ‖-(f a✝ ⊓ 0)‖ₑ

Proof state:
case h
α : 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✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(-f a✝).toNNReal = ‖-(f a✝ ⊓ 0)‖ₑ

Tactic:
congr 1

Result:
case h.e_a
α : 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✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ (-f a✝).toNNReal = ‖-(f a✝ ⊓ 0)‖₊

Proof state:
case h.e_a.a
α : 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✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ -f a✝ ⊔ 0 = ‖f a✝ ⊓ 0‖

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

Result:
no goals

Proof state:
case h.e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = ↑↑f₁ a✝ ⊔ 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ (f a✝).toNNReal = ‖f a✝ ⊔ 0‖₊

Tactic:
apply NNReal.eq

Result:
case h.e_a.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = ↑↑f₁ a✝ ⊔ 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(f a✝).toNNReal = ↑‖f a✝ ⊔ 0‖₊

Proof state:
case e_a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ‖↑↑(Lp.posPart f₁) a‖ₑ ∂μ

Tactic:
apply lintegral_congr_ae

Result:
case e_a.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
⊢ (fun a => ENNReal.ofReal (f a)) =ᶠ[ae μ] fun a => ‖↑↑(Lp.posPart f₁) a‖ₑ

Proof state:
case h.e_a.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = ↑↑f₁ a✝ ⊔ 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(f a✝).toNNReal = ↑‖f a✝ ⊔ 0‖₊

Tactic:
rw [Real.nnnorm_of_nonneg (le_max_right _ _)]

Result:
case h.e_a.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = ↑↑f₁ a✝ ⊔ 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(f a✝).toNNReal = ↑⟨f a✝ ⊔ 0, ⋯⟩

Proof state:
case e_a.h
α : 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₁‖
⊢ (fun a => ENNReal.ofReal (-f a)) =ᶠ[ae μ] fun a => ‖↑↑(Lp.negPart f₁) a‖ₑ

Tactic:
filter_upwards [Lp.coeFn_negPart f₁, hf.coeFn_toL1] with _ h₁ h₂

Result:
case h
α : 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✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ‖↑↑(Lp.negPart f₁) a✝‖ₑ