Tactics

The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword by.

Fin_cases

Perform cases on i : Fin n. Substitutes it with the explicit numerals 0, 1, 2, ...