-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpL2_indicator_eq_toSpanSingleton_comp (hm : m ≤ m0) (hs : MeasurableSet s)
    (hμs : μ s ≠ ∞) (x : E') : (condExpL2 E' 𝕜 hm (indicatorConstLp 2 hs hμs x) : α →₂[μ] E') =
    (toSpanSingleton ℝ x).compLp (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1))

Proof state:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
h_comp :
  ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a =>
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ] fun a =>
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)

Tactic:
filter_upwards with y using rfl

Result:
no goals

Proof state:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
⊢ ↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) =ᶠ[ae μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))

Tactic:
refine (condExpL2_indicator_ae_eq_smul 𝕜 hm hs hμs x).trans ?_

Result:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))

Proof state:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))

Tactic:
have h_comp := (toSpanSingleton ℝ x).coeFn_compLp
  (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α →₂[μ] ℝ)

Result:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
h_comp :
  ∀ᵐ (a : α) ∂μ,
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) a =
      (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))

Proof state:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
h_comp :
  ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a =>
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))

Tactic:
refine EventuallyEq.trans ?_ h_comp.symm

Result:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
h_comp :
  ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a =>
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ] fun a =>
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)

Proof state:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
h_comp :
  ∀ᵐ (a : α) ∂μ,
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) a =
      (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))

Tactic:
rw [← EventuallyEq] at h_comp

Result:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
h_comp :
  ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) =ᶠ[ae μ] fun a =>
    (toSpanSingleton ℝ x) (↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a)
⊢ (fun a => ↑↑↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x) =ᶠ[ae μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))

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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
⊢ ↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) =
    (toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))

Tactic:
ext1

Result:
case h
α : 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
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E'
⊢ ↑↑↑((condExpL2 E' 𝕜 hm) (indicatorConstLp 2 hs hμs x)) =ᶠ[ae μ]
    ↑↑((toSpanSingleton ℝ x).compLp ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))