case h
𝕜 : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
⊢ ↑(↑adjoint (comp A B)) v = ↑(comp (↑adjoint B) (↑adjoint A)) v
𝕜 : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
⊢ ↑adjoint (comp A B) = comp (↑adjoint B) (↑adjoint A)
ext v
case h
𝕜 : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
w : (fun x => E) v
⊢ inner w (↑(↑adjoint (comp A B)) v) = inner w (↑(comp (↑adjoint B) (↑adjoint A)) v)
case h
𝕜 : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
⊢ ↑(↑adjoint (comp A B)) v = ↑(comp (↑adjoint B) (↑adjoint A)) v
refine' ext_inner_left 𝕜 fun w => _
no goals
case h
𝕜 : Type u_1
E : Type u_4
F : Type u_2
G : Type u_3
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
w : (fun x => E) v
⊢ inner w (↑(↑adjoint (comp A B)) v) = inner w (↑(comp (↑adjoint B) (↑adjoint A)) v)
simp only [adjoint_inner_right, ContinuousLinearMap.coe_comp', Function.comp_apply]