mathlib3

0a865275 - Workaround: use assumption rather than apply_instance