case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.280924
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 : E →L[𝕜] F
v : E
⊢ ↑(↑adjointAux (↑adjointAux A)) v = ↑A v
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.280924
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 : E →L[𝕜] F
⊢ ↑adjointAux (↑adjointAux A) = A
ext v
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.280924
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 : E →L[𝕜] F
v : E
w : (fun x => F) v
⊢ inner w (↑(↑adjointAux (↑adjointAux A)) v) = inner w (↑A v)
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.280924
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 : E →L[𝕜] F
v : E
⊢ ↑(↑adjointAux (↑adjointAux A)) v = ↑A v
refine' ext_inner_left 𝕜 fun w => _
no goals
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.280924
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 : E →L[𝕜] F
v : E
w : (fun x => F) v
⊢ inner w (↑(↑adjointAux (↑adjointAux A)) v) = inner w (↑A v)
rw [adjointAux_inner_right, adjointAux_inner_left]