no goals
ι : Type ?u.1215956
ι' : Type u_3
𝕜 : Type u_2
inst✝¹⁰ : IsROrC 𝕜
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1215988
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1216006
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1216026
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : ι → E
inst✝ : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
i : { x // x ∈ s }
⊢ ↑(↑(OrthonormalBasis.span h s) i) = v' ↑i
simp only [OrthonormalBasis.span, Basis.span_apply, LinearIsometryEquiv.ofEq_symm,
  OrthonormalBasis.map_apply, OrthonormalBasis.coe_mk, LinearIsometryEquiv.coe_ofEq_apply,
  comp_apply]