-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq_norm_posPart_sub (f : α →₁ₛ[μ] ℝ) : integral f = ‖posPart f‖ - ‖negPart f‖

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝

Tactic:
rw [SimpleFunc.map_apply, h]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = ‖(toSimpleFunc f).posPart a✝‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ integral f = ‖posPart f‖ - ‖negPart f‖

Tactic:
have ae_eq₁ : (toSimpleFunc f).posPart =ᵐ[μ] (toSimpleFunc (posPart f)).map norm := by
  filter_upwards [posPart_toSimpleFunc f] with _ h
  rw [SimpleFunc.map_apply, h]
  conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
⊢ ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))

Tactic:
filter_upwards [negPart_toSimpleFunc f] with _ h

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
a✝ : α
h : (toSimpleFunc (negPart f)) a✝ = (toSimpleFunc f).negPart a✝
⊢ (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ (toSimpleFunc f) a✝ =
    (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝

Tactic:
rw [SimpleFunc.sub_apply, ← h₁, ← h₂]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ (toSimpleFunc f) a✝ = (toSimpleFunc f).posPart a✝ - (toSimpleFunc f).negPart a✝

Proof state:
case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))) μ

Tactic:
exact (SimpleFunc.integrable f).pos_part.congr ae_eq₁

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))

Tactic:
apply MeasureTheory.SimpleFunc.integral_congr (SimpleFunc.integrable f)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ ⇑(toSimpleFunc f) =ᶠ[ae μ]
    ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = ‖(toSimpleFunc f).posPart a✝‖

Tactic:
conv_lhs => rw [← SimpleFunc.posPart_map_norm, SimpleFunc.map_apply]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖

Tactic:
have ae_eq₂ : (toSimpleFunc f).negPart =ᵐ[μ] (toSimpleFunc (negPart f)).map norm := by
  filter_upwards [negPart_toSimpleFunc f] with _ h
  rw [SimpleFunc.map_apply, h]
  conv_lhs => rw [← SimpleFunc.negPart_map_norm, SimpleFunc.map_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ integral f = ‖posPart f‖ - ‖negPart f‖

Tactic:
rw [integral, norm_eq_integral, norm_eq_integral, ← SimpleFunc.integral_sub]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))) μ

case hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
⊢ ⇑(toSimpleFunc f).posPart =ᶠ[ae μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))

Tactic:
filter_upwards [posPart_toSimpleFunc f] with _ h

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc ℝ 1 μ)
a✝ : α
h : (toSimpleFunc (posPart f)) a✝ = (toSimpleFunc f).posPart a✝
⊢ (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝