-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
lemma MemLp.condExpL2_ae_eq_condExp' (hm : m ≤ m₀) (hf1 : Integrable f μ) (hf2 : MemLp f 2 μ)
    [SigmaFinite (μ.trim hm)] : condExpL2 E 𝕜 hm hf2.toLp =ᵐ[μ] μ[f | m]

Proof state:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ⊤
⊢ ∫ (x : α) in s, ↑↑(toLp f hf2) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
refine setIntegral_congr_ae (hm _ hs) ?_

Result:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(toLp f hf2) x = f x

Proof state:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(toLp f hf2) x = f x

Tactic:
filter_upwards [hf2.coeFn_toLp] with ω hω _ using hω

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
⊢ ↑↑↑((condExpL2 E 𝕜 hm) (toLp f hf2)) =ᶠ[ae μ] μ[f|m]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hm hf1
  (fun s hs htop ↦ integrableOn_condExpL2_of_measure_ne_top hm htop.ne _) (fun s hs htop ↦ ?_)
  (aestronglyMeasurable_condExpL2 hm _)

Result:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ⊤
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 E 𝕜 hm) (toLp f hf2)) x ∂μ = ∫ (x : α) in s, f x ∂μ

Proof state:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ⊤
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 E 𝕜 hm) (toLp f hf2)) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [integral_condExpL2_eq hm (hf2.toLp _) hs htop.ne]

Result:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁵ : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : μ s < ⊤
⊢ ∫ (x : α) in s, ↑↑(toLp f hf2) x ∂μ = ∫ (x : α) in s, f x ∂μ