Lean: turn a planar curve in a 3D inner product space into a curve in ℂ

Given ⟪γ t - γ 0, v⟫ = 0 and finrank ℝ E = 3: set P := (ℝ ∙ v)ᗮ. Its dimension is Submodule.finrank_orthogonal_span_singleton (needs Fact (finrank = 2+1) and FiniteDimensional.of_fact_finrank_eq_succ). Take b := (stdOrthonormalBasis ℝ P).reindex (finCongr hP) and φ := b.repr.trans Complex.orthonormalBasisOneI.repr.symm : P ≃ₗᵢ[ℝ] ℂ. Use the CLM Lm := φ.toContinuousLinearEquiv ∘L P.orthogonalProjectionOnto (the old orthogonalProjection is deprecated) and j := P.subtypeₗᵢ.comp φ.symm.toLinearIsometry, so δ := Lm ∘ (γ - γ 0) has no subtypes. Then j (Lm x) = x for x ∈ P (simp with orthogonalProjectionOnto_mem_subspace_eq_self), and so ‖Lm x‖ = ‖x‖ on P. Derivatives of P-valued curves stay in P: differentiate s ↦ ⟪v, f s⟫ ≡ 0 and use HasDerivAt.unique with hasDerivAt_const.