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`.
```lean
example (p : Prop) : ¬(p ↔ ¬p) := by itauto
```



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: digama0

Mathlib.lean

@@ -3849,6 +3849,7 @@ import Mathlib.Tactic.HaveI
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.HigherOrder
 import Mathlib.Tactic.Hint
+import Mathlib.Tactic.ITauto
 import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IntervalCases

Mathlib/Mathport/Syntax.lean

@@ -47,6 +47,7 @@ import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Group
 import Mathlib.Tactic.GuardHypNums
 import Mathlib.Tactic.Hint
+import Mathlib.Tactic.ITauto
 import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.Inhabit
@@ -185,10 +186,6 @@ syntax generalizingClause := " generalizing" (ppSpace ident)+
 /- S -/ syntax (name := induction'') "induction''" casesTarget
   (fixingClause <|> generalizingClause)? (" with" (ppSpace colGt withPattern)+)? : tactic
 
-syntax termList := " [" term,* "]"
-/- B -/ syntax (name := itauto) "itauto" (" *" <|> termList)? : tactic
-/- B -/ syntax (name := itauto!) "itauto!" (" *" <|> termList)? : tactic
-
 /- B -/ syntax (name := obviously) "obviously" : tactic
 
 /- S -/ syntax (name := prettyCases) "pretty_cases" : tactic
@@ -221,8 +218,8 @@ syntax termList := " [" term,* "]"
 
 /- M -/ syntax (name := unfoldCases) "unfold_cases " tacticSeq : tactic
 
-/- B -/ syntax (name := equivRw) "equiv_rw" (config)? (termList <|> (ppSpace term)) (location)? :
-  tactic
+/- B -/ syntax (name := equivRw) "equiv_rw" (config)?
+  ((" [" term,* "]") <|> (ppSpace term)) (location)? : tactic
 /- B -/ syntax (name := equivRwType) "equiv_rw_type" (config)? ppSpace term : tactic
 
 /- E -/ syntax (name := nthRwLHS) "nth_rw_lhs " num rwRuleSeq (location)? : tactic

Mathlib/Tactic.lean

@@ -91,6 +91,7 @@ import Mathlib.Tactic.HaveI
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.HigherOrder
 import Mathlib.Tactic.Hint
+import Mathlib.Tactic.ITauto
 import Mathlib.Tactic.InferParam
 import Mathlib.Tactic.Inhabit
 import Mathlib.Tactic.IntervalCases