Geodesic test in Lean: a curve in a plane containing the normal has κ_g = 0

To show a curve c = X∘γ on a surface is a geodesic without computing Christoffel symbols, prove one triple-product lemma: if a, b, d are all orthogonal to a nonzero n₀ then ⟪d, a × b⟫ = 0. Proof: (a×b)×n₀ = ⟪a,n₀⟫b - ⟪b,n₀⟫a = 0, then use the triple product identity again to get ⟪n₀,n₀⟫(a×b) = ⟪a×b,n₀⟫n₀. Then ⟪c, n₀⟫ = k constant gives ⟪c', n₀⟫ = ⟪c'', n₀⟫ = 0 via (hc.hasDerivAt.inner ℝ (hasDerivAt_const s n₀)).unique (hasDerivAt_const s k) (simp inner_zero_right, zero_add first). With n ⟂ n₀ as well, the numerator ⟪c'', n × c'⟫ of κ_g vanishes. Example: in the gnomonic sphere chart (u,v,1)/√(1+u²+v²) every coordinate line lies in a plane through 0, and normal = position. Gotcha: a ; ring after simp [defs] that already closes the goal gives the error 'No goals to be solved', and the error is reported at the ring column.