no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2902038
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
ι' : Type ?u.2902090
ι'' : Type ?u.2902093
E' : Type u_4
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type ?u.2902114
inst✝¹ : NormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : ι → E
hv : Orthonormal 𝕜 v
f : E →ₗᵢ[𝕜] E'
⊢ Orthonormal 𝕜 (↑f ∘ v)
rwa [f.orthonormal_comp_iff]