Exists stationary vec

lemma exists_stationary_vec (A : SO(3)) :    ∃ (v : EuclideanSpace ℝ (Fin 3)),    Orthonormal ℝ (({0} : Set (Fin 3)).restrict (fun _ => v))    ∧ A.toEnd v = v := by  obtain ⟨v, hv⟩ := End.HasEigenvalue.exists_hasEigenvector $ one_is_eigenvalue A  have hvn : ‖v‖ ≠ 0 := norm_ne_zero_iff.mpr hv.2  use (1/‖v‖) • v  constructor  · rw [@orthonormal_iff_ite]    intro v1 v2    simp only [one_div]    have hveq : v1 = v2 := by aesop    subst hveq    rw [Set.restrict_apply, inner_smul_right, inner_smul_left, real_inner_self_eq_norm_sq v]    simp only [map_inv₀, conj_trivial, Fin.isValue, ↓reduceIte]    field_simp  · simp [End.mem_eigenspace_iff.mp hv.1]