John's ellipsoid theorem in Lean without contact points or Lagrange multipliers

Avoid the contact-point decomposition. Normalize the maximal ellipsoid to the unit ball B. If x ∈ K with ‖x‖ = R > d, the map stretch u α β = β•id + (α-β)•(innerSL ℝ u).smulRight u (u = x/R), shifted by ε•u, sends B into K. Prove that by contradiction: geometric_hahn_banach_closed_point gives f, convert it with (InnerProductSpace.toDual ℝ E).symm f to w, and use ⟪w, A z⟫ = ⟪A w, z⟫ ≤ ‖A w‖ with ‖A w‖² = β²‖w‖² + (α²-β²)⟪u,w⟫². The comparison with max(‖w‖, R⟪u,w⟫) is two polynomial identities, each closed with linear_combination. For det = α β^(d-1), get an orthonormal basis b with b 0 = u from Orthonormal.exists_orthonormalBasis_extension_of_card_eq (index Fin (n+1), s = {0}, v = fun _ => u, orthonormality via ⟨fun _ => hu, fun i j h => absurd (Subsingleton.elim i j) h⟩). Then rewrite LinearMap.toMatrix to Matrix.diagonal and finish with det_diagonal and Fin.prod_univ_succ. For existence, use compactness of {(c, A) : E × (E →L[ℝ] E) | ∀ z ∈ B, c + A z ∈ K}; the bound ‖A‖ ≤ 2ρ comes from ContinuousLinearMap.opNorm_le_of_unit_norm, and ContinuousLinearMap.continuous_det gives continuity. For det of a composition, rewrite with ContinuousLinearMap.toLinearMap_comp and then LinearMap.det_comp.