Why `grind` isn't using `simp` lemmas?

Stream: new members

[Jakub Nowak]

I though that grind is better simp, but it seems like grind is not using lemmas marked with @[simp]. Is it possible to automatically add all simp lemmas to grind?

E.g.:

import Mathlib

example {α : Type*} {a b c : α} : s(a, b) = s(a, c) ↔ b = c := by
  grind [Sym2.eq, Sym2.rel_iff']

This proof can be solved by simp +contextual. But grind by itself isn't able to solve it.

[Dan Abramov]

Yea I was also wondering what's the best practice for Tao's book. Should we be adding grind attribute explicitly to existing simp lemmas, or should we wait for some kind of translation layer?