I can’t find any information online about the simp! tactic, although it is suggested by the autocomplete function on VSCode. I’ve tried using it and it seems to work differently from simp, but while I can trace the definition of simp back to its source file, this doesn’t seem possible for simp!. Is this some syntax I don’t know about? Where can I find more information about this?
>Solution :
/-- `simp!` is shorthand for `simp` with `autoUnfold := true`.
This will rewrite with all equation lemmas, which can be used to
partially evaluate many definitions. -/