Curves in EuclideanSpace ℝ (Fin 3): componentwise derivatives and inner products

For fun s ↦ !₂[f₀ s, f₁ s, f₂ s] prove HasDerivAt by first doing the plain Pi version with rw [hasDerivAt_pi]; intro i; fin_cases i <;> simpa (lemma lives in Mathlib.Analysis.Calculus.Deriv.Prod), then compose with (EuclideanSpace.equiv (Fin 3) ℝ).symm.toContinuousLinearMap.hasFDerivAt.comp_hasDerivAt. To match a prescribed derivative like κ • N s, use (that lemma).congr_deriv ?_ and then ext i; fin_cases i <;> simp — convert … using 1 also creates a function-equality goal on which ext fails with 'failed to synthesize Fintype ℝ'. Inner products: simp [EuclideanSpace.inner_eq_star_dotProduct, Fin.sum_univ_three, dotProduct]; norms: EuclideanSpace.norm_eq, Real.sqrt_eq_one. In first | ring | … use ring1: ring does not fail when it cannot close the goal (it falls back to ring_nf), so first never tries the next alternative.