Simultaneous avoidance of the top homogeneous form, a tangent hyperplane, and a chosen coordinate hyperplane, by a direction over the base field.

theorem CCDN.exists_good_hypersurface_direction_with_coordinate {K : Type u_1} {σ : Type u_2} [Field K] [Infinite K] [Fintype σ] (f : MvPolynomial σ K) (hf : f ≠ 0) (z : σ → K) (j : σ) (hj : (MvPolynomial.eval z) ((MvPolynomial.pderiv j) f) ≠ 0) (k : σ) : ∃ (b : σ → K), b k ≠ 0 ∧ (MvPolynomial.eval b) ((MvPolynomial.homogeneousComponent f.totalDegree) f) ≠ 0 ∧ ∑ i : σ, (MvPolynomial.eval z) ((MvPolynomial.pderiv i) f) * b i ≠ 0

Over an infinite field, a smooth point admits a direction with nonzero leading form, nonzero directional derivative, and nonzero selected coordinate.