7.1. Example use case🔗

We already saw the interactive mode at the very beginning. Let's look at the example again to figure out why we needed interactive mode:

theorem exists_subset_or_subset_of_two_mul_lt_card'
    {α : Type*} [DecidableEq α] {X Y : Finset α} {n : ℕ}
    (hXY : 2 * n < #(X ∪ Y)) :
    ∃ C : Finset α, n < #C ∧ (C ⊆ X ∨ C ⊆ Y) := byα:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)
  grind =>
    have : #(X ∪ Y) = #X + #(Y \ X)grindα:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)h✝:∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Ythis:#(X ∪ Y) = #X + #(Y \ X)⊢ False
    finishAll goals completed! 🐙

We should first figure out what lemmas grind uses to prove the intermediate step. We can do this for example as follows:

theorem exists_subset_or_subset_of_two_mul_lt_card''
    {α : Type*} [DecidableEq α] {X Y : Finset α} {n : ℕ}
    (hXY : 2 * n < #(X ∪ Y)) :
    ∃ C : Finset α, n < #C ∧ (C ⊆ X ∨ C ⊆ Y) := byα:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)
  grind =>
    have : #(X ∪ Y) = #X + #(Y \ X) := byα:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)h✝:∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Y⊢ #(X ∪ Y) = #X + #(Y \ X) Try these:
  [apply] grind only [usr card_union_add_card_inter, usr card_sdiff_add_card_inter]
  [apply] grind =>
    instantiate only [usr card_union_add_card_inter]
    instantiate only [usr card_sdiff_add_card_inter]
    instantiate only [usr card_union_add_card_inter]
    acgrind?All goals completed! 🐙
    finishAll goals completed! 🐙

which gives us the following output

Try these:
  [apply] grind only [usr card_union_add_card_inter, usr card_sdiff_add_card_inter]
  [apply] grind =>
    instantiate only [usr card_union_add_card_inter]
    instantiate only [usr card_sdiff_add_card_inter]
    instantiate only [usr card_union_add_card_inter]
    ac

So we can see that grind uses the lemmas Finset.card_union_add_card_inter and Finset.card_union_add_card_inter. The usr tells us that is uses patterns manually specified via grind_pattern.

We can now look for these patterns in Mathlib. We find:

grind_pattern card_union_add_card_inter => #(s ∪ t), s ∩ t
grind_pattern card_union_add_card_inter => s ∪ t, #(s ∩ t)
grind_pattern card_union_add_card_inter => #(s ∪ t), #s
grind_pattern card_union_add_card_inter => #(s ∪ t), #t
grind_pattern card_union_add_card_inter => #(s ∩ t), #s
grind_pattern card_union_add_card_inter => #(s ∩ t), #t

and

grind_pattern card_sdiff_add_card_inter =>
  #(s \ t), #(s ∩ t)
grind_pattern card_sdiff_add_card_inter => #(s \ t), #s

So we can see that both of these theorems won't be considered if there is neither a union, nor an intersection, nor a difference of sets present. This means that this example uses interactive mode to guide e-matching.