Adding `@[grind →]` to `List.sizeOf_lt_of_mem`

Stream: lean4

[Mai]

Could we add @[grind →] to List.sizeOf_lt_of_mem? This is somewhat of a painpoint when trying to quickly prove termination of mutually recursive functions (see #general > Showing termination for mutually recursive definitions ).

[Yury G. Kudryashov]

docs#List.sizeOf_lt_of_mem to save others a few clicks.

[Jovan Gerbscheid]

I get the impression that we should wait for core to figure this out themselves so that grind knows about such theorems automatically.