𝕜 : Type u_2
E : Type u_1
F : Type ?u.826219
G : Type ?u.826222
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
⊢ id 𝕜 E = ↑adjoint (id 𝕜 E)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.826219
G : Type ?u.826222
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
⊢ ↑adjoint (id 𝕜 E) = id 𝕜 E
refine' Eq.symm _
𝕜 : Type u_2
E : Type u_1
F : Type ?u.826219
G : Type ?u.826222
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
⊢ ∀ (x : E) (y : (fun x => E) x), inner (↑(id 𝕜 E) x) y = inner x (↑(id 𝕜 E) y)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.826219
G : Type ?u.826222
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
⊢ id 𝕜 E = ↑adjoint (id 𝕜 E)
rw [eq_adjoint_iff]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.826219
G : Type ?u.826222
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
⊢ ∀ (x : E) (y : (fun x => E) x), inner (↑(id 𝕜 E) x) y = inner x (↑(id 𝕜 E) y)
simp