mathlib3

69054f82 - trying to use the simplifier rather than chain/rewrite

trying to use the simplifier rather than chain/rewrite why are the side goals being created? and why does it fail on the second example? the profiler says all the time is in infer_instance