mathlib3

9bc01784 - fix(tactic/finish): fix one classical leak, document another (#1929)

fix(tactic/finish): fix one classical leak, document another (#1929) * fix(tactic/finish): fix one classical leak, document another * fix(src/tactic): deprecate intuitionistic versions in docstrings. Closes #1927. Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>