feat: improve error messages of tauto (#5965)

Modify `tauto` to throw an error message "tauto failed to solve some goals" if it fails.

Author: joneugster

Mathlib/Lean/Elab/Tactic/Basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2023 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn
+Authors: Floris van Doorn, Jon Eugster
 -/
 import Mathlib.Lean.Meta
 /-!
@@ -18,4 +18,27 @@ Remark: note that `MVarId.getType'` uses `whnf` instead of `cleanupAnnotations`,
 def getMainTarget'' : TacticM Expr := do
   (← getMainGoal).getType''
 
+/--
+Like `done` but takes a scope (e.g. a tactic name) as an argument
+to produce more detailed error messages.
+-/
+def doneWithScope (scope : MessageData) : TacticM Unit := do
+  let gs ← getUnsolvedGoals
+  unless gs.isEmpty do
+    logError m!"{scope} failed to solve some goals.\n"
+    Term.reportUnsolvedGoals gs
+    throwAbortTactic
+
+/--
+Like `focusAndDone` but takes a scope (e.g. tactic name) as an argument to
+produce more detailed error messages.
+-/
+def focusAndDoneWithScope (scope : MessageData) (tactic : TacticM α) : TacticM α :=
+  focus do
+    let a ← try tactic catch e =>
+      if isAbortTacticException e then throw e
+      else throwError "{scope} failed.\n{← nestedExceptionToMessageData e}"
+    doneWithScope scope
+    pure a
+
 end Lean.Elab.Tactic

Mathlib/Tactic/Tauto.lean

@@ -190,14 +190,13 @@ def finishingConstructorMatcher (e : Q(Prop)) : MetaM Bool :=
   | _ => pure false
 
 /-- Implementation of the `tauto` tactic. -/
-def tautology : TacticM Unit := focus do
+def tautology : TacticM Unit := focusAndDoneWithScope "tauto" do
   evalTactic (← `(tactic| classical!))
   tautoCore
   allGoals (iterateUntilFailure
     (evalTactic (← `(tactic| rfl)) <|>
      evalTactic (← `(tactic| solve_by_elim)) <|>
      liftMetaTactic (constructorMatching · finishingConstructorMatcher)))
-  done
 
 /--
 `tauto` breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`