-- Mathlib/MeasureTheory/Function/SpecialFunctions/Inner.lean
theorem AEMeasurable.inner {m : MeasurableSpace α} [MeasurableSpace E] [OpensMeasurableSpace E]
    [SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f g : α → E}
    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (fun x => ⟪f x, g x⟫) μ

Proof state:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
x : α
hxg : g x = mk g hg x
hxf : f x = mk f hf x
⊢ (fun x => Inner.inner (f x) (g x)) x = (fun x => Inner.inner (mk f hf x) (mk g hg x)) x

Tactic:
dsimp only

Result:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
x : α
hxg : g x = mk g hg x
hxf : f x = mk f hf x
⊢ Inner.inner (f x) (g x) = Inner.inner (mk f hf x) (mk g hg x)

Proof state:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
x : α
hxg : g x = mk g hg x
hxf : f x = mk f hf x
⊢ Inner.inner (f x) (g x) = Inner.inner (mk f hf x) (mk g hg x)

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (fun x => Inner.inner (f x) (g x)) μ

Tactic:
refine ⟨fun x => ⟪hf.mk f x, hg.mk g x⟫, hf.measurable_mk.inner hg.measurable_mk, ?_⟩

Result:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ (fun x => Inner.inner (f x) (g x)) =ᵐ[μ] fun x => Inner.inner (mk f hf x) (mk g hg x)

Proof state:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ (fun x => Inner.inner (f x) (g x)) =ᵐ[μ] fun x => Inner.inner (mk f hf x) (mk g hg x)

Tactic:
refine hf.ae_eq_mk.mp (hg.ae_eq_mk.mono fun x hxg hxf => ?_)

Result:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
m : MeasurableSpace α
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : SecondCountableTopology E
μ : MeasureTheory.Measure α
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
x : α
hxg : g x = mk g hg x
hxf : f x = mk f hf x
⊢ (fun x => Inner.inner (f x) (g x)) x = (fun x => Inner.inner (mk f hf x) (mk g hg x)) x