case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ inner (↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) (↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =
    ∫ (x : α), ↑(starRingEnd ((fun a => 𝕜) x)) (↑f x) * ↑g x ∂μ
apply integral_congr_ae
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
have hf_ae := f.coeFn_toLp 2 μ 𝕜
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
have hg_ae := g.coeFn_toLp 2 μ 𝕜
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
a✝ : α
hf : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝ = ↑f a✝
hg : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝ = ↑g a✝
⊢ inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝) =
    ↑(starRingEnd 𝕜) (↑f a✝) * ↑g a✝
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
filter_upwards [hf_ae, hg_ae] with _ hf hg
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
a✝ : α
hf : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝ = ↑f a✝
hg : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝ = ↑g a✝
⊢ inner (↑f a✝) (↑g a✝) = ↑(starRingEnd 𝕜) (↑f a✝) * ↑g a✝
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
a✝ : α
hf : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝ = ↑f a✝
hg : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝ = ↑g a✝
⊢ inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝) =
    ↑(starRingEnd 𝕜) (↑f a✝) * ↑g a✝
rw [hf, hg]
no goals
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
a✝ : α
hf : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝ = ↑f a✝
hg : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝ = ↑g a✝
⊢ inner (↑f a✝) (↑g a✝) = ↑(starRingEnd 𝕜) (↑f a✝) * ↑g a✝
simp