no goals
ι : Type u_1
ι' : Type ?u.1598118
𝕜 : Type u_3
inst✝¹¹ : IsROrC 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
E' : Type ?u.1598147
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : InnerProductSpace 𝕜 E'
F : Type ?u.1598165
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : InnerProductSpace ℝ F
F' : Type ?u.1598185
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : InnerProductSpace ℝ F'
inst✝² : Fintype ι
v✝ : Set E
A : ι → Submodule 𝕜 E
inst✝¹ : DecidableEq ι
h : IsInternal A
α : ι → Type u_4
inst✝ : (i : ι) → Fintype (α i)
hV : OrthogonalFamily 𝕜 (fun i => { x // x ∈ A i }) fun i => subtypeₗᵢ (A i)
v : (i : ι) → OrthonormalBasis (α i) 𝕜 { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(collectedOrthonormalBasis hV h v) a ∈ A a.fst
simp [DirectSum.IsInternal.collectedOrthonormalBasis]