5.1. General🔗

An expression is indexable if it starts with a constant that is anything but Eq, HEq, Iff, And, Or and Not. For example, an expression of the form t = s where t and s are some subexpressions cannot be used as a pattern.

In addition to simply looking whether a single pattern can be found in the context, theorems can also have multi-patterns. Here multiple patterns need to be found in the context before the theorem is applied.

Here is a theorem in Mathlib where a multi-pattern is used:

theorem card_ne_zero_of_mem {α : Type*} {s : Finset α}
    {a : α} (h : a ∈ s) : #s ≠ 0 :=
  (not_congr card_eq_zero).2 <| ne_empty_of_mem h

Let us consider the different patterns we could use here. We cannot use #s ≠ 0 or #s = 0 because both of these start with a non-indexable constant. We could use #s as a pattern. However, this doesn't mention a, so the theorem would be tried whenever we talk about the cardinality of a finite set even when there is no element in the context. We also probably don't want to try to apply this theorem whenever a statement of the form a ∈ s is on the whiteboard because in this case we don't know if we need to consider cardinalities at all.

So Mathlib specifies the multi-pattern a ∈ s, #s here. So the fact that #s ≠ 0 will be added to the context, whenever there is a statement of the form a ∈ s on the whiteboard and somewhere on the whiteboard the cardinality of s is mentioned.

It is important to note that a multi-pattern is not the same as specifying multiple patterns. In a multi-pattern all included patterns need to match. When multiple patterns are specified, one of them needs to match in order for the theorem to be used.