Exists nonzero solution

lemma exists_nonzero_solution (k n m : ℕ) (ωs : Fin n ↪ F) (f : Fin n → F) :    ∃ c : (weigthBoundIndices k (proximity_gap_degree_bound k n m)) → F,    c ≠ 0 ∧ constraintMap k n m ωs f (proximity_gap_degree_bound k n m) c = 0 := by      have h_kernel_nontrivial : Module.finrank F ((weigthBoundIndices k        (proximity_gap_degree_bound k n m)) → F) >          Module.finrank F ((Fin n → constraintIndices m → F)) := by        convert numVars_gt_numConstraints k n m using 1        · simp [numVars]        · simp [numConstraints]          norm_num [Module.finrank]      have h_inj : ¬ Function.Injective          (constraintMap k n m ωs f (proximity_gap_degree_bound k n m)) := by        intro h_inj        exact h_kernel_nontrivial.not_ge          (LinearMap.finrank_range_of_inj h_inj ▸ Submodule.finrank_le _)      contrapose! h_inj      exact LinearMap.ker_eq_bot.mp (eq_bot_iff.mpr fun x hx ↦        by_contra fun hx' ↦ h_inj x hx' <| by simpa using hx)