mathlib3

41dd70c8 - apply_instance to get around convert bug