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

Proof state:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : RCLike 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g
a✝ : α
hf : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a✝ = f a✝
hg : ↑↑((ContinuousMap.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 μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ (fun a => inner (↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ] fun a =>
    (starRingEnd 𝕜) (f a) * g a

Tactic:
have hf_ae := f.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ

Result:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : RCLike 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
⊢ (fun a => inner (↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑((ContinuousMap.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 μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g
⊢ (fun a => inner (↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑((ContinuousMap.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 μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g
a✝ : α
hf : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a✝ = f a✝
hg : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a✝ = g a✝
⊢ inner (↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a✝) (↑↑((ContinuousMap.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 μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
⊢ (fun a => inner (↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ] fun a =>
    (starRingEnd 𝕜) (f a) * g a

Tactic:
have hg_ae := g.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ

Result:
case h
α : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : RCLike 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g
⊢ (fun a => inner (↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑((ContinuousMap.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 μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g
a✝ : α
hf : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a✝ = f a✝
hg : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a✝ = g a✝
⊢ inner (↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a✝) (↑↑((ContinuousMap.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 μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f
hg_ae : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g
a✝ : α
hf : ↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a✝ = f a✝
hg : ↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a✝ = g a✝
⊢ inner (f a✝) (g a✝) = (starRingEnd 𝕜) (f a✝) * g a✝

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : RCLike 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ inner ((ContinuousMap.toLp 2 μ 𝕜) f) ((ContinuousMap.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 μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ (fun a => inner (↑↑((ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑((ContinuousMap.toLp 2 μ 𝕜) g) a)) =ᶠ[ae μ] fun a =>
    (starRingEnd 𝕜) (f a) * g a