mathlib3

feat(tactic/use): apply exists_prop after use

#1882

Merged