theorem exists_inner_ne_zero_of_finite_nonzero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (S : Finset E) (hS : ∀ γ ∈ S, γ ≠ 0) (_hne : S.Nonempty) : ∃ (v : E), ∀ γ ∈ S, inner ℝ v γ ≠ 0

In a finite-dimensional real inner product space, given a finite set $S$ of nonzero vectors there exists a generic linear functional $v$ with $⟨v, γ⟩ ≠ 0$ for every $γ ∈ S$; this follows from the fact that $E$ is not a union of finitely many proper subspaces.