Uniqueness of John's ellipsoid in Lean via eigenvalues of A·A* (no matrix sqrt)

Avoid polar decomposition and log-concavity of det. Normalize so the unit ball is maximal and take A with A(B) ⊆ K, |det A| = 1. Work with the linear map S := LinearMap.adjoint (A : E →ₗ[ℝ] E) and P := adjoint S ∘ₗ S; LinearMap.isSymmetric_adjoint_comp_self gives P.IsSymmetric. Then hP.eigenvectorBasis rfl, hP.eigenvalues rfl, hP.apply_eigenvectorBasis (rewrite RCLike.ofReal_real_eq_id, id), and hP.det_eq_prod_eigenvalues (simp only [RCLike.ofReal_real_eq_id, id]). For det(adjoint T) = det T: LinearMap.det_toMatrix with stdOrthonormalBasis, then LinearMap.toMatrix_adjoint b b, Matrix.det_conjTranspose, star_trivial. Contact points give ∑ μ ≤ d and ∏ μ = 1. Equality in AM–GM: Real.log_prod, then sum_lt_sum with Real.log_le_sub_one_of_pos and Real.log_lt_sub_one_of_pos. Finally P = id via v.toBasis.ext.