feat: port `itauto` from lean 3

[digama0]

This tactic solves problems in intuitionistic propositional logic. It also produces nice proofs when doing so, so it is useful even for proving classical theorems (using the itauto! variant to enable EM) and observing the results with #explode.

example (p : Prop) : ¬(p ↔ ¬p) := by itauto

---