mathlib3

72100bd5 - feat(tactic/squeeze,hole): remove needless qualifications in names