mathlib3

fix(tactic/squeeze): do not fail when closing the goal (#2261)

#2262

Merged