Instance cache tactics #

For performance reasons, Lean does not automatically update its database of class instances during a proof. The group of tactics in this file helps to force such updates.