chore: remove last use of classical! (#12257)

The `classical!` tactic is always replaceable by the `classical` tactic. This removes the last use of it, which required adding in Std the plumbing-level implementation of `classical`. - [x] Depends on: #12256 Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Apr 19, 2024 · 6096b4a · 6096b4a
1 parent 11f79c5
commit 6096b4a
Showing 1 changed file with 7 additions and 7 deletions.
diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean
@@ -15,7 +15,7 @@ The `tauto` tactic.
 
 namespace Mathlib.Tactic.Tauto
 
-open Lean Elab.Tactic Parser.Tactic Lean.Meta MVarId
+open Lean Elab.Tactic Parser.Tactic Lean.Meta MVarId Std.Tactic
 open Qq
 
 initialize registerTraceClass `tauto
@@ -186,12 +186,12 @@ def finishingConstructorMatcher (e : Q(Prop)) : MetaM Bool :=
 
 /-- Implementation of the `tauto` tactic. -/
 def tautology : TacticM Unit := focusAndDoneWithScope "tauto" do
-  evalTactic (← `(tactic| classical!))
-  tautoCore
-  allGoals (iterateUntilFailure
-    (evalTactic (← `(tactic| rfl)) <|>
-     evalTactic (← `(tactic| solve_by_elim)) <|>
-     liftMetaTactic (constructorMatching · finishingConstructorMatcher)))
+  classical do
+    tautoCore
+    allGoals (iterateUntilFailure
+      (evalTactic (← `(tactic| rfl)) <|>
+      evalTactic (← `(tactic| solve_by_elim)) <|>
+      liftMetaTactic (constructorMatching · finishingConstructorMatcher)))
 
 /--
 `tauto` breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`