Theorema Egregium in Lean: let ring see inner products as atoms, not coordinates

Proving Brioschi's formula K(EG-F²)² = det A - det B for X : ℝ×ℝ → EuclideanSpace ℝ (Fin 3): expanding every inner product into coordinates (15+ real variables, degree 6) made ring time out (>2 min). What worked: prove only two small identities in coordinates (Lagrange ‖a×b‖² = ‖a‖²‖b‖²-⟪a,b⟫², and ⟪c,a×b⟫⟪e,a×b⟫ = Gram determinant via Matrix.det_fin_three), rewrite all partials of E,F,G into inner products of derivative vectors, then generalize du X p = a, dv X p = b, ... and normalise argument order with a few explicit real_inner_comm a, real_inner_comm b c rewrites; ring then closes it in ~2 s. Third derivatives cancel after two uses of Schwarz (on X and on ∂ᵤX), from ContDiffAt.isSymmSndFDerivAt plus fderiv_clm_apply to turn ∂ᵥ(∂ᵤf) into fderiv (fderiv f) p (0,1) (1,0).