-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpL2_const_inner (hm : m ≤ m0) (f : Lp E 2 μ) (c : E) :
    condExpL2 𝕜 𝕜 hm (((Lp.memLp f).const_inner c).toLp fun a => ⟪c, f a⟫) =ᵐ[μ]
    fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫

Proof state:
case refine_1
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
s : Set α
a✝ : MeasurableSet s
hμs : μ s < ⊤
⊢ IntegrableOn (↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp)) s μ

Tactic:
rw [IntegrableOn, integrable_congr (ae_restrict_of_ae h_eq)]

Result:
case refine_1
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
s : Set α
a✝ : MeasurableSet s
hμs : μ s < ⊤
⊢ Integrable (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) (μ.restrict s)

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
⊢ ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)

Tactic:
have h_eq : h_mem_Lp.toLp _ =ᵐ[μ] fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫ :=
  h_mem_Lp.coeFn_toLp

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)

Proof state:
case refine_3
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯))) μ

Tactic:
exact lpMeas.aeStronglyMeasurable _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
⊢ MemLp (↑↑↑((condExpL2 E 𝕜 hm) f)) 2 μ

Tactic:
exact Lp.memLp _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)

Tactic:
refine EventuallyEq.trans ?_ h_eq

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) =ᶠ[ae μ]
    ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp)

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) =ᶠ[ae μ]
    ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp)

Tactic:
refine Lp.ae_eq_of_forall_setIntegral_eq' 𝕜 hm _ _ two_ne_zero ENNReal.coe_ne_top
  (fun s _ hμs => integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _) ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ⊤ → IntegrableOn (↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp)) s μ

case refine_2
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ⊤ →
        ∫ (x : α) in s, ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) x ∂μ =
          ∫ (x : α) in s, ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) x ∂μ

case refine_3
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ AEStronglyMeasurable (↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯))) μ

case refine_4
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
⊢ AEStronglyMeasurable (↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp)) μ