fix(test/*): make sure tests produce no output (#3947)
Modify tests so that they produce no output. This also means removing all uses of `sorry`/`admit`.
Replace `#eval` by `run_cmd` consistently.
Tests that produced output before are modified so that it is checked that they roughly produce the right output
Add a trace option to the `#simp` command that turns the message of only if the expression is simplified to `true`. All tests are modified so that they simplify to `true`.
The randomized tests can produce output when they find a false positive, but that should basically never happen.
Add some docstings to `src/tactic/interactive`.
