Commit 2024-06-12 18:41 9035d155
View on Github →feat: port itauto from lean 3 (#9398)
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