Various clean ups

- Remove 'prove' tactic
- Remove some duplicated tactics and make some proofs more efficient
3 jobs for master in 1 minute (queued for 2 seconds)