ulift instances for groups and monoids
This file defines instances for group, monoid, semigroup and related structures on
ulift α is just a "copy" of a type
α in a higher universe.)
tactic.pi_instance_derive_field, even though it wasn't intended for this purpose,
which seems to work fine.