library_search and negation

[PatrickMassot]

The change below is unfortunately needed.

import tactic

lemma my_nice_lemma : 5 ≠ 1 := by norm_num

example : ¬ 5 = 1 :=
begin
  -- change 5 ≠ 1,
  library_search,
end

[bryangingechen]

Interestingly, library_search! now works and returns Try this: exact of_to_bool_ff rfl.

[PatrickMassot]

This library_search! "fix" is pure luck because the lemma is rfl. It doesn't work with

import tactic

constant x : ℕ 
constant y : ℕ

axiom my_nice_lemma : x ≠ y

example : ¬ x = y :=
begin
  -- change x ≠ y,
  library_search!,
end