-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem setIntegral_abs_condExp_le {s : Set α} (hs : MeasurableSet[m] s) (f : α → ℝ) :
    ∫ x in s, |(μ[f|m]) x| ∂μ ≤ ∫ x in s, |f x| ∂μ

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[s.indicator f|m]) x| ∂μ
⊢ ∫ (x : α), |(μ[s.indicator f|m]) x| ∂μ ≤ ∫ (x : α), s.indicator (fun x => |f x|) x ∂μ

Tactic:
refine (integral_abs_condExp_le _).trans
  (le_of_eq <| integral_congr_ae <| Eventually.of_forall fun x => ?_)

Result:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[s.indicator f|m]) x| ∂μ
x : α
⊢ (fun x => |s.indicator f x|) x = s.indicator (fun x => |f x|) x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : (fun x => |(μ[s.indicator f|m]) x|) =ᶠ[ae μ] fun x => |s.indicator (μ[f|m]) x|
⊢ (s.indicator fun x => |(μ[f|m]) x|) =ᶠ[ae μ] fun x => |(μ[s.indicator f|m]) x|

Tactic:
refine EventuallyEq.trans (Eventually.of_forall fun x => ?_) this.symm

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : (fun x => |(μ[s.indicator f|m]) x|) =ᶠ[ae μ] fun x => |s.indicator (μ[f|m]) x|
x : α
⊢ s.indicator (fun x => |(μ[f|m]) x|) x = |s.indicator (μ[f|m]) x|

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
⊢ (s.indicator fun x => |(μ[f|m]) x|) =ᶠ[ae μ] fun x => |(μ[s.indicator f|m]) x|

Tactic:
have : (fun x => |(μ[s.indicator f|m]) x|) =ᵐ[μ] fun x => |s.indicator (μ[f|m]) x| :=
  (condExp_indicator hfint hs).fun_comp abs

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : (fun x => |(μ[s.indicator f|m]) x|) =ᶠ[ae μ] fun x => |s.indicator (μ[f|m]) x|
⊢ (s.indicator fun x => |(μ[f|m]) x|) =ᶠ[ae μ] fun x => |(μ[s.indicator f|m]) x|

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ

Tactic:
have : ∫ x in s, |(μ[f|m]) x| ∂μ = ∫ x, |(μ[s.indicator f|m]) x| ∂μ := by
  rw [← integral_indicator (hnm _ hs)]
  refine integral_congr_ae ?_
  have : (fun x => |(μ[s.indicator f|m]) x|) =ᵐ[μ] fun x => |s.indicator (μ[f|m]) x| :=
    (condExp_indicator hfint hs).fun_comp abs
  refine EventuallyEq.trans (Eventually.of_forall fun x => ?_) this.symm
  rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
  simp only [Real.norm_eq_abs]

Result:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[s.indicator f|m]) x| ∂μ
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ