1. Basic usage of grind🔗

The grind tactic is meant to automatically provide proofs for easy goals.

Here are some examples where grind is used to prove simple lemmas in Mathlib:

The tactic appears very frequently in Mathlib to close simple side goals.

There is also a grind interactive mode that is still used very rarely in Mathlib.

Here is one example of its use in Mathlib:

This proof does not work without the interactive mode:

This is what the ouput looks like when grind fails:

`grind` failed
grind.2α:Type u_1inst:DecidableEq αX Y:Finset αn:ℕhXY:2 * n < #(X ∪ Y)h:∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Yleft:¬X ∪ Y ⊆ Xright:¬X ∪ Y ⊆ Yw:αh_3:¬(w ∈ X ∪ Y → w ∈ X)w_1:αh_5:¬(w_1 ∈ X ∪ Y → w_1 ∈ Y)⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] 2 * n + 1 ≤ #(X ∪ Y)
[prop] ∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Y
[prop] #(X ∪ Y) ≤ n ∨ ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y
[prop] (X ∪ Y ⊆ Y) = ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ Y
[prop] (X ∪ Y ⊆ X) = ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ X
[prop] ¬X ∪ Y ⊆ X
[prop] ¬X ∪ Y ⊆ Y
[prop] ¬(w ∈ X ∪ Y → w ∈ X)
[prop] ¬(w_1 ∈ X ∪ Y → w_1 ∈ Y)
[prop] w_1 ∈ X ∪ Y → ¬#(X ∪ Y) = 0
[prop] w ∈ X ∪ Y → ¬#(X ∪ Y) = 0
[prop] (w_1 ∈ X ∪ Y) = (w_1 ∈ X ∨ w_1 ∈ Y)
[prop] (w ∈ X ∪ Y) = (w ∈ X ∨ w ∈ Y)
[eqc] True propositions
[prop] 2 * n + 1 ≤ #(X ∪ Y)
[prop] ∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Y
[prop] ¬X ∪ Y ⊆ X
[prop] ¬X ∪ Y ⊆ Y
[prop] ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y
[prop] #(X ∪ Y) ≤ n ∨ ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y
[prop] (X ∪ Y ⊆ X) = ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ X
[prop] (X ∪ Y ⊆ Y) = ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ Y
[prop] w ∈ X ∪ Y
[prop] w_1 ∈ X ∪ Y
[prop] ¬#(X ∪ Y) = 0
[prop] w ∈ X ∨ w ∈ Y
[prop] w_1 ∈ X ∨ w_1 ∈ Y
[prop] (w ∈ X ∪ Y) = (w ∈ X ∨ w ∈ Y)
[prop] (w_1 ∈ X ∪ Y) = (w_1 ∈ X ∨ w_1 ∈ Y)
[prop] w_1 ∈ X
[prop] w ∈ Y
[prop] w ∈ X ∪ Y → ¬#(X ∪ Y) = 0
[prop] w_1 ∈ X ∪ Y → ¬#(X ∪ Y) = 0
[eqc] False propositions
[prop] X ∪ Y ⊆ X
[prop] X ∪ Y ⊆ Y
[prop] w ∈ X
[prop] w_1 ∈ Y
[prop] ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ X
[prop] ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ Y
[prop] w ∈ X ∪ Y → w ∈ X
[prop] w_1 ∈ X ∪ Y → w_1 ∈ Y
[prop] #(X ∪ Y) = 0
[cases] Case analyses
[cases] [2/2]: #(X ∪ Y) ≤ n ∨ ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y
[cases] source: E-matching `h`
[ematch] E-matching patterns
[thm] card_union_add_card_inter: [@card #3 (@Union.union (Finset _) _ #1 #0), @card _ #0]
[thm] card_union_add_card_inter: [@card #3 (@Union.union (Finset _) _ #1 #0), @card _ #1]
[thm] h: [@LE.le `[ℕ] `[instLENat] (@card `[α] #0) `[n]]
[thm] h: [@card `[α] #0]
[thm] h: [@Subset `[Finset α] `[instHasSubset] #0 `[X]]
[thm] h: [@Subset `[Finset α] `[instHasSubset] #0 `[Y]]
[thm] subset_iff: [@Subset (Finset #2) _ #1 #0]
[thm] Set.subset_def: [@Subset _ _ #1 #0]
[thm] card_ne_zero_of_mem: [@Membership.mem #3 (Finset _) _ #2 #1, @card _ #2]
[thm] mem_union: [@Membership.mem #4 (Finset _) _ (@Union.union (Finset _) _ #2 #1) #0]
[thm] Multiset.mem_add: [@Membership.mem #3 _ _ (@HAdd.hAdd _ _ _ _ #1 #0) #2]
[thm] Set.mem_union: [@Membership.mem #3 _ _ (@Union.union _ _ #1 #0) #2]
[thm] HtmlFeatures.mem_union: [@Membership.mem `[HtmlFeature] `[HtmlFeatures] `[HtmlFeatures.instMembershipHtmlFeature] (@Union.union `[HtmlFeatures] `[HtmlFeatures.instUnion] #1 #0) #2]
[thm] HtmlFeatures.mem_iff_contains: [@Membership.mem `[HtmlFeature] `[HtmlFeatures] `[HtmlFeatures.instMembershipHtmlFeature] #1 #0]
[cutsat] Assignment satisfying linear constraints
[assign] n := 0
[assign] #(X ∪ Y) := 1

[grind] Diagnostics
[thm] E-Matching instances
[thm] card_ne_zero_of_mem ↦ 2
[thm] mem_union ↦ 2
[thm] subset_iff ↦ 2
[thm] h ↦ 1

We will come back later to this example to figure out why this doesn't work and how to read the error message.

Similar to simp, you can write grind? to receive a squeezed grind call that limits which lemmas are used and on which terms splits are performed.

In our first example from above we get the suggestions:

Try these:
  [apply] grind only [= Int.even_iff]
  [apply] grind => instantiate only [= Int.even_iff]

You can see that it displays the necessary lemma used here. We will learn what the "=" means later.

Sometimes the output will be a little more confusing:

Try these:
  [apply] grind only [#d39b]
  [apply] grind only
  [apply] grind => cases #d39b <;> done

You can see that this uses a so called "anchor" to refer to parts of the context that grind performed a case split on. Unfortunately these don't show hover information here. They do however in interactive mode. We can use finish? like this:

To get a suggestion for a proof which does display the following information for the anchor: (∀ (b : α), b ∈ s → ¬a = b) = (a ∈ s). So we can see that grind performed a split on whether the equivalent propositions are each true or not.