-- 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_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 (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) μ

Tactic:
exact (lpMeas.aeStronglyMeasurable _).const_inner

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
⊢ ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)

Tactic:
have h_mem_Lp : MemLp (fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫) 2 μ := by
  refine MemLp.const_inner _ ?_; exact Lp.memLp _

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 μ
⊢ ↑↑↑((condExpL2 𝕜 𝕜 hm) (MemLp.toLp (fun a => inner c (↑↑f a)) ⋯)) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)

Proof state:
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 ∂μ

Tactic:
intro s hs hμs

Result:
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 α
hs : MeasurableSet s
hμ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 ∂μ

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 α),
    MeasurableSet s →
      μ s < ⊤ → IntegrableOn (↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp)) s μ

Tactic:
intro s _ hμs

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 < ⊤
⊢ IntegrableOn (↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp)) s μ

Proof state:
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 α
hs : MeasurableSet s
hμ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 ∂μ

Tactic:
rw [integral_condExpL2_eq_of_fin_meas_real _ hs hμs.ne,
  integral_congr_ae (ae_restrict_of_ae h_eq), ←
  L2.inner_indicatorConstLp_eq_setIntegral_inner 𝕜 (↑(condExpL2 E 𝕜 hm f)) (hm s hs) c hμs.ne,
  ← inner_condExpL2_left_eq_right, condExpL2_indicator_of_measurable _ hs,
  L2.inner_indicatorConstLp_eq_setIntegral_inner 𝕜 f (hm s hs) c hμs.ne,
  setIntegral_congr_ae (hm s hs)
    ((MemLp.coeFn_toLp ((Lp.memLp f).const_inner c)).mono fun x hx _ => hx)]

Result:
no goals

Proof state:
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)) μ

Tactic:
refine AEStronglyMeasurable.congr ?_ h_eq.symm

Result:
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 (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) μ

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 (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ

Tactic:
refine MemLp.const_inner _ ?_

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
⊢ MemLp (↑↑↑((condExpL2 E 𝕜 hm) f)) 2 μ