leanprover support

[jaredgreen2]

add support for interactions specific to the lean plugin, such as reading tactic states at any given point in the code and calling power tactics(exact?, aesop, duper, canonical when that becomes available, omega, grind, tauto, auto, bv_decide, etc.) if available.