no goals
ι : Type ?u.1342675
ι' : Type ?u.1342678
𝕜 : Type ?u.1342681
inst✝⁹ : IsROrC 𝕜
E : Type ?u.1342687
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1342707
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.1342745
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : OrthonormalBasis (Fin 2) ℝ F
f : F
⊢ ↑(LinearIsometryEquiv.symm (isometryOfOrthonormal v)) f =
    ↑(↑(Basis.coord (OrthonormalBasis.toBasis v) 0) f) + ↑(↑(Basis.coord (OrthonormalBasis.toBasis v) 1) f) * I
simp [Complex.isometryOfOrthonormal]