-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem integral_condExp (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] :
    ∫ x, (μ[f|m]) x ∂μ = ∫ x, f x ∂μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : ¬Integrable f μ
⊢ ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
simp only [condExp_of_not_integrable hf, Pi.zero_apply, integral_zero, integral_undef hf]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ ∫ (x : α) in Set.univ, (μ[f|m]) x ∂μ = ∫ (x : α) in Set.univ, f x ∂μ

Tactic:
exact setIntegral_condExp hm hf .univ

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : ¬Integrable f μ
⊢ ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ
⊢ ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
exact this

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
suffices ∫ x in Set.univ, (μ[f|m]) x ∂μ = ∫ x in Set.univ, f x ∂μ by
  simp_rw [setIntegral_univ] at this; exact this

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ ∫ (x : α) in Set.univ, (μ[f|m]) x ∂μ = ∫ (x : α) in Set.univ, f x ∂μ

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : ∫ (x : α) in Set.univ, (μ[f|m]) x ∂μ = ∫ (x : α) in Set.univ, f x ∂μ
⊢ ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
simp_rw [setIntegral_univ] at this

Result:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ
⊢ ∫ (x : α), (μ[f|m]) x ∂μ = ∫ (x : α), f x ∂μ