feat: fix some issues with equals t => tac

Batteries/Tactic/Init.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 module
 
 public meta import Lean.Elab.Tactic.ElabTerm
+public meta import Lean.Meta.MatchUtil
 
 public meta section
 
@@ -110,5 +111,12 @@ example (P : (Nat → Nat) → Prop) : P (fun n => n - n) := by
   -- current goal: P (fun n => 0)
 ```
 -/
-macro (name := Conv.equals) "equals " t:term " => " tac:tacticSeq : conv =>
-  `(conv| tactic => show (_ = $t); next => $tac)
+elab (name := Conv.equals) "equals " t:term " => " tac:tacticSeq : conv => do
+  let mvarId ← getMainGoal
+  mvarId.withContext do
+    let goal ← mvarId.getType
+    let some (α, _, rhs) ← matchEq? goal | throwError "invalid 'conv' goal"
+    let e ← Term.withSynthesize do
+      Term.elabTermEnsuringType t (some α)
+    unless ← isDefEq rhs e do throwError m!"failed to resolve{indentExpr rhs}\n=?={indentExpr e}"
+    evalTactic <| ← `(conv| tactic => · $tac)

BatteriesTest/conv_equals.lean

@@ -41,3 +41,33 @@ example (P : (Nat → Nat) → Prop) : P (fun n => n - n) := by
     -- and at this point, there should be no goal left
     tactic => sorry
   sorry
+
+/-- warning: declaration uses 'sorry' -/
+#guard_msgs in
+example (P : Nat → Prop) : P 12 := by
+  conv =>
+    enter [1]
+    equals (12 : Fin 37) =>
+      guard_target =ₛ (12 : Nat) = (12 : Fin 37)
+      rfl
+  guard_target =ₛ P (12 : Fin 37)
+  sorry
+
+/--
+error: Type mismatch
+  12
+has type
+  Nat
+but is expected to have type
+  Fin 37
+---
+error: unsolved goals
+P : Fin 37 → Prop
+⊢ 12 = sorry
+-/
+#guard_msgs in
+example (P : Fin 37 → Prop) : P 12 := by
+  conv =>
+    enter [1]
+    equals (12 : Nat) => skip
+  sorry