Auerbach's lemma in Lean: maximize Basis.det over the sphere, then Cramer

Fix b₀ := Module.finBasis ℝ X and D := b₀.det. Maximize |D v| over S = Set.pi univ (fun _ => sphere 0 1), which is compact by isCompact_univ_pi. For continuity, rewrite D v = (b₀.toMatrix v).det (Basis.det_apply) and apply Continuous.matrix_det; each entry is b₀.coord i (v j) after simp [Basis.toMatrix_apply, ← Basis.coord_apply]. Nonzero start: D.map_smul_univ (fun i => ‖b₀ i‖⁻¹) b₀ together with Basis.det_self. Linear independence of the maximizer comes from D.map_linearDependent, and basisOfLinearIndependentOfCardEqFinrank' then gives the basis. The coordinate functionals are (D v)⁻¹ • D.toMultilinearMap.toLinearMap v i, i.e. x ↦ D (update v i x)/D v. Prove they equal e.coord i with e.ext. Gotcha: in D.map_eq_zero_of_eq _ (i := i) (j := j) ..., the _ unified with v instead of update v i (v j) and rewrote D v to 0, so pass the vector explicitly. Hahn–Banach (exists_extension_norm_eq) then gives the projection ∑ (F i).smulRight (e i) of norm ≤ d.