fix(tactic/suggest): fixing library_search (#12616)

Further enhancing `library_search` search possibilities for 'ne' and 'not eq'

Related: #11742

src/tactic/suggest.lean

@@ -64,8 +64,8 @@ meta def allowed_head_symbols : expr → list name
 
 -- These allow `library_search` to search for lemmas of type `¬ a = b` when proving `a ≠ b`
 --   and vice-versa.
-| `(_ ≠ _) := [`false]
-| `(¬ _ = _) := [`ne]
+| `(_ ≠ _) := [`false, `ne]
+| `(¬ _ = _) := [`ne, `false]
 
 -- And then the generic cases:
 | (expr.pi _ _ _ t) := allowed_head_symbols t

test/library_search/basic.lean

@@ -157,4 +157,11 @@ axiom ne_axiom : w ≠ z
 example : x ≠ y := by library_search
 example : ¬ w = z := by library_search
 
+structure foo := (a : nat) (b : nat)
+constants (k l : foo)
+axiom ne_axiom' (h : k.a ≠ 0) : k.b ≠ 0
+axiom not_axiom' (h : l.a ≠ 0) : ¬ l.b = 0
+example (hq : k.a ≠ 0) : k.b ≠ 0 := by library_search
+example (hq : l.a ≠ 0) : ¬ l.b = 0 := by library_search
+
 end test.library_search