mathlib

e7bd3127 - chore(tactic/pi_instance): add a docstring, remove a little bit of redundancy (#2500)