no goals
𝕜 : Type u_2
E : Type u_3
F : Type ?u.3085209
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
ι' : Type u_4
ι'' : Type ?u.3085264
E' : Type u_5
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type ?u.3085285
inst✝¹ : NormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ↑v
v' : Basis ι' 𝕜 E'
hv' : Orthonormal 𝕜 ↑v'
e : ι ≃ ι'
i : ι'
⊢ ↑(equiv hv hv' e) (↑(LinearIsometryEquiv.symm (equiv hv hv' e)) (↑v' i)) =
    ↑(equiv hv hv' e) (↑(equiv hv' hv e.symm) (↑v' i))
simp only [LinearIsometryEquiv.apply_symm_apply, Orthonormal.equiv_apply, e.apply_symm_apply]