simp priority

Stream: mathlib4

[Yury G. Kudryashov]

In Lean 3, lemmas explicitly listed in simp [lemma1, lemma2] had higher priority than all lemmas marked with simp (probably, they were added to the top of the stack). It would be nice to forward-port this behavior (e.g., by assigning them a huge priority).

[Yury G. Kudryashov]

Sometimes, I used this assumption about simp to override @[simp] lemmas (e.g., use docs#not_and_distrib instead of the default docs#not_and).

[Yury G. Kudryashov]

When I port this code, I have to squeeze these simps now.