-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem integral_condExpL2_eq (hm : m ≤ m0) (f : Lp E' 2 μ) (hs : MeasurableSet[m] s)
    (hμs : μ s ≠ ∞) : ∫ x in s, (condExpL2 E' 𝕜 hm f : α → E') x ∂μ = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 E' 𝕜 hm) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ

Tactic:
rw [← sub_eq_zero, ←
  integral_sub' (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs)
    (integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs)]

Result:
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∫ (a : α) in s, (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) a ∂μ = 0

Proof state:
case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ Integrable (↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) (μ.restrict s)

Tactic:
rw [integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub (↑(condExpL2 E' 𝕜 hm f)) f).symm)]

Result:
case refine_1
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ Integrable (↑↑(↑((condExpL2 E' 𝕜 hm) f) - f)) (μ.restrict s)

Proof state:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
⊢ ∫ (a : α) in s, inner c (↑↑↑((condExpL2 E' 𝕜 hm) f) a) ∂μ - ∫ (a : α) in s, inner c (↑↑f a) ∂μ = 0

Tactic:
have h_ae_eq_f := MemLp.coeFn_toLp (E := 𝕜) ((Lp.memLp f).const_inner c)

Result:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
h_ae_eq_f : ↑↑(MemLp.toLp (fun a => inner c (↑↑f a)) ⋯) =ᶠ[ae μ] fun a => inner c (↑↑f a)
⊢ ∫ (a : α) in s, inner c (↑↑↑((condExpL2 E' 𝕜 hm) f) a) ∂μ - ∫ (a : α) in s, inner c (↑↑f a) ∂μ = 0

Proof state:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
h_ae_eq_f : ↑↑(MemLp.toLp (fun a => inner c (↑↑f a)) ⋯) =ᶠ[ae μ] fun a => inner c (↑↑f a)
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a => inner c (↑↑f a)) ⋯) x ∂μ

Tactic:
exact integral_condExpL2_eq_of_fin_meas_real _ hs hμs

Result:
no goals

Proof state:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
h_ae_eq_f : ↑↑(MemLp.toLp (fun a => inner c (↑↑f a)) ⋯) =ᶠ[ae μ] fun a => inner c (↑↑f a)
⊢ ∫ (a : α) in s, inner c (↑↑↑((condExpL2 E' 𝕜 hm) f) a) ∂μ - ∫ (a : α) in s, inner c (↑↑f a) ∂μ = 0

Tactic:
rw [sub_eq_zero, ←
  setIntegral_congr_ae (hm s hs) ((condExpL2_const_inner hm f c).mono fun x hx _ => hx), ←
  setIntegral_congr_ae (hm s hs) (h_ae_eq_f.mono fun x hx _ => hx)]

Result:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
h_ae_eq_f : ↑↑(MemLp.toLp (fun a => inner c (↑↑f a)) ⋯) =ᶠ[ae μ] fun a => inner c (↑↑f a)
⊢ ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a => inner c (↑↑f a)) ⋯) x ∂μ

Proof state:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
⊢ ∫ (x : α) in s, inner c ((↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) x) ∂μ = 0

Tactic:
simp_rw [Pi.sub_apply, inner_sub_right]

Result:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
⊢ ∫ (x : α) in s, inner c (↑↑↑((condExpL2 E' 𝕜 hm) f) x) - inner c (↑↑f x) ∂μ = 0

Proof state:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
⊢ ∫ (x : α) in s, inner c (↑↑↑((condExpL2 E' 𝕜 hm) f) x) - inner c (↑↑f x) ∂μ = 0

Tactic:
rw [integral_sub
    ((integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs).const_inner c)
    ((integrableOn_Lp_of_measure_ne_top _ fact_one_le_two_ennreal.elim hμs).const_inner c)]

Result:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
⊢ ∫ (a : α) in s, inner c (↑↑↑((condExpL2 E' 𝕜 hm) f) a) ∂μ - ∫ (a : α) in s, inner c (↑↑f a) ∂μ = 0

Proof state:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
⊢ ∀ (c : E'), ∫ (x : α) in s, inner c ((↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) x) ∂μ = 0

Tactic:
intro c

Result:
case refine_2
α : Type u_1
E' : Type u_3
𝕜 : Type u_7
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
f : ↥(Lp E' 2 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E'
⊢ ∫ (x : α) in s, inner c ((↑↑↑((condExpL2 E' 𝕜 hm) f) - ↑↑f) x) ∂μ = 0