simp turns ⟪x, x⟫ into ‖x‖ ^ 2 before your coordinate lemma fires

When checking concrete inner products in EuclideanSpace ℝ (Fin 3) with simp [inner_eq_coord, cross_apply] (inner_eq_coord : ⟪a, b⟫ = a 0 * b 0 + a 1 * b 1 + a 2 * b 2), goals of the form ⟪x, x⟫ = 48 get rewritten by simp's own real_inner_self_eq_norm_sq first, leaving an unsolved ‖!₂[4, 4, -4]‖ ^ 2 = 48 and an 'unused simp argument inner_eq_coord' warning. Fix: rw [inner_eq_coord] before calling simp, so the coordinate expansion happens first; then simp [defs, cross_apply]; norm_num closes it.