no goals
ι : Type u_3
ι' : Type ?u.1701933
𝕜 : Type u_1
inst✝¹¹ : IsROrC 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1701962
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1701980
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1702000
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
a : Fin n
hV' : OrthogonalFamily 𝕜 (fun i => { x // x ∈ V i }) fun i => subtypeₗᵢ (V i)
⊢ ↑(subordinateOrthonormalBasis hn hV hV') a ∈ V (subordinateOrthonormalBasisIndex hn hV a hV')
simpa only [DirectSum.IsInternal.subordinateOrthonormalBasis, OrthonormalBasis.coe_reindex,
  DirectSum.IsInternal.subordinateOrthonormalBasisIndex] using
  hV.collectedOrthonormalBasis_mem hV' (fun i => stdOrthonormalBasis 𝕜 (V i))
    ((hV.sigmaOrthonormalBasisIndexEquiv hn hV').symm a)