-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem BoundedContinuousFunction.inner_toLp (f g : α →ᵇ 𝕜) :
    ⟪BoundedContinuousFunction.toLp (E := 𝕜) 2 μ 𝕜 f,
        BoundedContinuousFunction.toLp (E := 𝕜) 2 μ 𝕜 g⟫ =
      ∫ x, conj (f x) * g x ∂μ

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ inner ((BoundedContinuousFunction.toLp 2 μ 𝕜) f) ((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =
    ∫ (x : α), (starRingEnd 𝕜) (f x) * g x ∂μ

Tactic:
apply integral_congr_ae

Result:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ (fun a =>
      inner (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ]
    fun a => (starRingEnd 𝕜) (f a) * g a

Proof state:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
⊢ (fun a =>
      inner (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ]
    fun a => (starRingEnd 𝕜) (f a) * g a

Tactic:
have hg_ae := g.coeFn_toLp 2 μ 𝕜

Result:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g
⊢ (fun a =>
      inner (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ]
    fun a => (starRingEnd 𝕜) (f a) * g a

Proof state:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑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✝

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g
⊢ (fun a =>
      inner (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ]
    fun a => (starRingEnd 𝕜) (f a) * g a

Tactic:
filter_upwards [hf_ae, hg_ae] with _ hf hg

Result:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑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✝

Proof state:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ (fun a =>
      inner (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ]
    fun a => (starRingEnd 𝕜) (f a) * g a

Tactic:
have hf_ae := f.coeFn_toLp 2 μ 𝕜

Result:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
⊢ (fun a =>
      inner (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ]
    fun a => (starRingEnd 𝕜) (f a) * g a

Proof state:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑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✝

Tactic:
rw [hf, hg]

Result:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
inst✝¹ : RCLike 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑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✝