mathlib3

feat(tactics/interactive): choose uses exists_prop

#1014

Merged