mathlib3

fix(tactic/finish): fix one classical leak, document another

#1929

Merged