We define the
measurability tactic using
measurability? solves goals of the form
AEStronglyMeasurable f μ, or
MeasurableSet s by applying lemmas tagged
measurability user attribute, and suggests a faster proof script that can be substituted
for the tactic call in case of success.