5.5. Figuring out lemmas that should be tagged🔗

When a grind call that you expect should work actually fails this could be due to missing tagged lemmas. In this case you can either identify yourself which lemmas the proof should use and which ones of those are (insufficiently) tagged. Alternatively, you can use grind +suggestions which also considers lemmas for e-matching that have not been tagged.

Here is an example from Mathlib that has a proof using grind and a lemma that isn't tagged with a grind attribute:

@[simp]
theorem isAdjMatrix_adjMatrix (α : Type*) {V : Type*}
    (G : SimpleGraph V) [DecidableRel G.Adj] [Zero α]
    [One α] : (G.adjMatrix α).IsAdjMatrix where
  zero_or_one := byα:Type u_1V:Type u_2G:SimpleGraph Vinst✝²:DecidableRel G.Adjinst✝¹:Zero αinst✝:One α⊢ ∀ (i j : V), SimpleGraph.adjMatrix α G i j = 0 ∨ SimpleGraph.adjMatrix α G i j = 1 grind [SimpleGraph.adjMatrix_apply]All goals completed! 🐙

If you were trying to come up with this proof, you could for example do the following:

@[simp]
theorem isAdjMatrix_adjMatrix' (α : Type*) {V : Type*}
    (G : SimpleGraph V) [DecidableRel G.Adj] [Zero α]
    [One α] : (G.adjMatrix α).IsAdjMatrix where
  zero_or_one := byα:Type u_1V:Type u_2G:SimpleGraph Vinst✝²:DecidableRel G.Adjinst✝¹:Zero αinst✝:One α⊢ ∀ (i j : V), SimpleGraph.adjMatrix α G i j = 0 ∨ SimpleGraph.adjMatrix α G i j = 1 Try these:
  [apply] grind only [SimpleGraph.adjMatrix_apply, #8bc53232e5fd58f8]
  [apply] grind only [SimpleGraph.adjMatrix_apply]
  [apply] grind =>
    instantiate only [SimpleGraph.adjMatrix_apply]
    cases #8bc53232e5fd58f8grind? +suggestionsAll goals completed! 🐙

which outputs

Try these:
  [apply] grind only [SimpleGraph.adjMatrix_apply, #8bc53232e5fd58f8]
  [apply] grind only [SimpleGraph.adjMatrix_apply]
  [apply] grind =>
    instantiate only [SimpleGraph.adjMatrix_apply]
    cases #8bc53232e5fd58f8

Then you can consider whether this lemma should possibly be tagged.

In this case, the lemma SimpleGraph.adjMatrix_apply features a case distinction on the right side and should therefore not be tagged per the rule above.