8.1. Local grind
As mentioned before, one needs to be careful to not tag too many lemmas. However, sometimes there are lemmas that are too general for a global grind lemmas but are convenient to use on a smaller scale. For example, when setting up the basic theory around a definition, one might want to unfold specific definitions or use certain basic lemmas.
For theorems this is facilitated the following way: you can tag a theorem with @[local grind *] (where * is a pattern modifier) or use local grind_pattern to specify a grind pattern as usual but allow it to only be used in the file where it is defined. Here is an example from Mathlib (the comments are part of Mathlib as well):
theorem Finset.card_le_card' {α : Type*} {s t : Finset α} :
s ⊆ t → #s ≤ #t :=
Multiset.card_le_card ∘ val_le_iff.mpr
-- This pattern is unreasonable to use generally,
-- but it's convenient in this file.
-- (Note that we turn it on again later in this file.)
local grind_pattern Finset.card_le_card' => #s, #t
To use definitions locally you can use the grind tactic with +locals. This allows grind to unfold all definitions from the current file. It is a little hard to include an example here. But you can find one in Mathlib here.