This file defines all the tactics that are required by mathport. Most of the syntax declarations in this file (as opposed to the imported files) are not defined anywhere and effectively form the TODO list before we can port mathlib to lean 4 for real.

For tactic writers: I (Mario) have put a comment before each syntax declaration to represent the estimated difficulty of writing the tactic. The key is as follows: