Guide to grind_pattern

Stream: lean4

[Wrenna Robson]

I have an odd case where I have some theorem myTheorem (unfortunately hard to give a good MWE here), which I tag with grind, but it doesn't use it as I expect, but if I add @myTheorem to my local context it manages to do so.

This is a bit weird, and I am wondering if what I should do is define a new grind pattern or something because it can't work out how to apply this theorem (the conclusion of the theorem is a[i] < n, where a is of some type with a GetElem defined, and this applies basically everywhere the GetElem is define).

Is there a good guide to defining grind patterns anywhere (and advice as to why one might do this?)

[Kim Morrison]

https://lean-lang.org/doc/reference/latest/The--grind--tactic/E___matching/#e-matching

[Wrenna Robson]

Thank you