mathlib

e3c8b7d4 - elab_simple to the rescue