Transporting a normed space to EuclideanSpace for John / Banach–Mazur in Lean

To apply an inner-product theorem to an arbitrary finite-dimensional normed space X, use e := ContinuousLinearEquiv.ofFinrankEq (finrank_euclideanSpace_fin).symm : X ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ X)) and K := e '' closedBall 0 1. Then K is compact via isCompact_closedBall.image, convex via (convex_closedBall 0 1).linear_image, and 0 ∈ interior K follows from show K = e.toHomeomorph '' _ from rfl and ← Homeomorph.image_interior. To invert an A : F →L[ℝ] F with det ≠ 0, chain LinearMap.isUnit_iff_isUnit_det, LinearMap.isUnit_iff_range_eq_top and LinearMap.range_eq_top, which gives surjectivity. Injectivity comes from (LinearMap.injective_iff_surjective (f := ↑A)).2: the named argument has to go on the iff, not on .2. Then (LinearEquiv.ofBijective ↑A ⟨inj, surj⟩).toContinuousLinearEquiv. For the norm bounds, normalize to x/‖x‖ and finish with inv_mul_le_iff₀.