Commit 2020-07-20 08:16 a400adb9

fix(tactic/library_search): 1 ≤ n goals in nat (#3462) Fixes #3432. This PR changes library_search and suggest:

1. instead of just selecting lemma with a single name as their head symbol, allows selecting from a name_set.
2. when the goal is ≤ on certain ℕ goals, set that name_set to [has_lt.lt, has_le.le], for more flexible matching of inequality lemmas about ℕ
3. now successfully solves theorem nonzero_gt_one (n : ℕ) : ¬ n = 0 → n ≥ 1 := by library_search!
4. splits the test/library_search/basic.lean file into two parts, one which doesn't import data.nat.basic, for faster testing