mathlib3

28dc2ed5 - fix(tactic/suggest): normalize synonyms uniformly in goal and lemma (#2829)

fix(tactic/suggest): normalize synonyms uniformly in goal and lemma (#2829) This change is intended to make `library_search` and `suggest` a bit more robust in unfolding the types of the goal and lemma in order to determine which lemmas it will try to apply. Before, there were two ad-hoc systems to map a head symbol to the name(s) that it should match, now there is only one ad-hoc function that does so. As a consequence, `library_search` should be able to use a lemma with return type `a > b` to close the goal `b < a`, and use `lemma foo : p → false` to close the goal `¬ p`. (The `>` normalization shouldn't "really" be needed if we all strictly followed the `gt_or_ge` linter but we don't and the failure has already caused confusion.) [Discussion on Zulip starts here](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20to.20get.20familiar.20enough.20with.20Mathlib.20to.20use.20it/near/198746479)