Links: [[Coq]] - `apply` make use of a theorem / lemma. (how?) - `auto` (`eauto`) - `cbn` (`simpl`) reduce to a semi-normal form. Tries to leave things still readable rather than in fully normal form. `cbn` is the more principled, faster and more predictable replacement to `simpl`. https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.cbn - `constructor` - `destruct` - `intro` (`intros`) - `inversion` - `rewrite` Given an equality in context and a conclusion that matches one side of the equality, swap the conclusion for the other side - `simpl` see `cbn`