All Options in Mathlib4 all options version of lean mathlib4 version This is a list of mathlib4 options. How to obtain this Get the output of #help tactic. Replace syntax ^option (regex) with ### option.