have library_search call symmetry before giving up

[semorrison]

Often library_search fails to find a lemma just because the user has written an equation backwards relative to how it appears in mathlib. One option would be to just do a second pass after calling symmetry on the goal. Possibly better would be to do this on a "per lemma" basis.

[robertylewis]

This seems to have been implemented in #2415

import tactic.suggest

constants P Q : Prop 

axiom pq : P ↔ Q 

example : Q ↔ P := by library_search

constants a b : ℕ

axiom ab : a = b 

example : b = a := by library_search