case h.e'_3.a
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : IsWellOrder ι fun x x_1 => x < x_1
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst✝ : DecidableEq ι
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) x✝) (f x✝) =
    Basis.toMatrix (OrthonormalBasis.toBasis (gramSchmidtOrthonormalBasis h f)) f x✝ x✝
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : IsWellOrder ι fun x x_1 => x < x_1
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst✝ : DecidableEq ι
⊢ ↑(Basis.det (OrthonormalBasis.toBasis (gramSchmidtOrthonormalBasis h f))) f =
    ∏ i : ι, inner (↑(gramSchmidtOrthonormalBasis h f) i) (f i)
convert Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)
no goals
case h.e'_3.a
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : IsROrC 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : IsWellOrder ι fun x x_1 => x < x_1
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
inst✝ : DecidableEq ι
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ inner (↑(gramSchmidtOrthonormalBasis h f) x✝) (f x✝) =
    Basis.toMatrix (OrthonormalBasis.toBasis (gramSchmidtOrthonormalBasis h f)) f x✝ x✝
exact ((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f _) _).symm