fix: make sure #guard_* uses syntactic equality

src/Lean/Elab/Tactic/Guard.lean

@@ -19,7 +19,7 @@ have to be to pass the tactic.
 This inductive gives the different specifiers that can be selected.
 -/
 inductive MatchKind
-/-- A syntactic match means that the `Expr`s are `==` after stripping `MData` -/
+/-- A syntactic match means that the `Expr`s are `=` after stripping `MData` -/
 | syntactic
 /-- A defeq match `isDefEqGuarded` returns true. (Note that unification is allowed here.) -/
 | defEq (red : TransparencyMode := .reducible)
@@ -54,7 +54,7 @@ def equal.toMatchKind : TSyntax ``equal → Option MatchKind
 
 /-- Applies the selected matching rule to two expressions. -/
 def MatchKind.isEq (a b : Expr) : MatchKind → MetaM Bool
-  | .syntactic => return a.consumeMData == b.consumeMData
+  | .syntactic => return a.consumeMData.equal b.consumeMData
   | .alphaEq => return a.eqv b
   | .defEq red => withoutModifyingState <| withTransparency red <| Lean.Meta.isDefEqGuarded a b
 

tests/lean/run/3943.lean

@@ -5,12 +5,12 @@ example (f : Nat → Nat) : (if f x = 0 then f x else f x + 1) + f x = y := by
 
 example (f : Nat → Nat) : f x = 0 → f x + 1 = y := by
   simp (config := { contextual := true })
-  guard_target =ₛ f x = 0 → 1 = y
+  guard_target =ₐ f x = 0 → 1 = y
   sorry
 
 example (f : Nat → Nat) : let _  : f x = 0 := sorryAx _ false; f x + 1 = y := by
   simp (config := { contextual := true, zeta := false })
-  guard_target =ₛ let _  : f x = 0 := sorryAx _ false; 1 = y
+  guard_target =ₐ let _ : f x = 0 := sorryAx _ false; 1 = y
   sorry
 
 def overlap : Nat → Nat
@@ -20,20 +20,20 @@ def overlap : Nat → Nat
 
 example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n  := by
   simp (config := { contextual := true }) only [overlap]
-  guard_target =ₛ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n
+  guard_target =ₐ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n
   sorry
 
 example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n  := by
   -- The following tactic should because the default discharger only uses assumptions available
   -- when `simp` was invoked unless `contextual := true`
   fail_if_success simp only [overlap]
-  guard_target =ₛ (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n
+  guard_target =ₐ (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n
   sorry
 
 example : (if (n = 0 → False) then overlap (n+1) else overlap (n+1)) = overlap n  := by
   -- assumption is not a well-behaved discharger, and the following should still work as expected
   simp (discharger := assumption) only [overlap]
-  guard_target =ₛ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n
+  guard_target =ₐ (if (n = 0 → False) then overlap n else overlap (n+1)) = overlap n
   sorry
 
 opaque p : Nat → Bool
@@ -47,5 +47,5 @@ example : (if p x then g x else g x + 1) + g x = y := by
 
 example : (let _  : p x := sorryAx _ false; g x + 1 = y) ↔ g x = y := by
   simp (config := { zeta := false }) (discharger := assumption)
-  guard_target =ₛ (let _  : p x := sorryAx _ false; x + 1 = y) ↔ g x = y
+  guard_target =ₐ (let _ : p x := sorryAx _ false; x + 1 = y) ↔ g x = y
   sorry

tests/lean/run/6065.lean

@@ -11,7 +11,7 @@ def foo (r : Nat) : Nat :=
 
 example {r : Nat} : foo r = 0 := by
   simp only [foo.eq_def]
-  guard_target =ₛ
+  guard_target =ₐ
     (match r with
         | Nat.zero => 0
         | l@h:(Nat.succ n) =>

tests/lean/run/6263.lean

@@ -5,10 +5,10 @@ open Lean.Elab.Tactic
 variable (p q : Prop)
 theorem foo (h : p ∧ q) : q ∧ p := by
   run_tac liftMetaTactic1 (·.revertAll)
-  guard_target =ₛ ∀ (p q : Prop), p ∧ q → q ∧ p
+  guard_target =ₐ ∀ (p q : Prop), p ∧ q → q ∧ p
   sorry
 
 theorem bla (h : p ∧ q) : q ∧ p := by
   revert p q
-  guard_target =ₛ ∀ (p q : Prop), p ∧ q → q ∧ p
+  guard_target =ₐ ∀ (p q : Prop), p ∧ q → q ∧ p
   sorry

tests/lean/run/grind_canon_insts.lean

@@ -80,7 +80,7 @@ warning: declaration uses 'sorry'
 example (a b c d : Nat) : b * a = d * b → False := by
   rw [CommMonoid.mul_comm d b] -- Introduces a new (non-canonical) instance for `Mul Nat`
   -- See target here
-  guard_target =ₛ
+  guard_target =ₐ
     @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a
     =
     @HMul.hMul Nat Nat Nat (@instHMul Nat (@Semigroup.toMul Nat (@Monoid.toSemigroup Nat (@CommMonoid.toMonoid Nat instCommMonoidNat)))) b d

tests/lean/run/grind_revertAll.lean

@@ -13,7 +13,7 @@ elab "ensure_no_mvar" : tactic => do
 example {α : Type u} [Inhabited α] (a : α) (f : α → α) (h : f a = default) : default = f a := by
   revert_all
   ensure_no_mvar
-  guard_target =ₛ∀ {α : Type u} [inst : Inhabited α] (a : α) (f : α → α), f a = default → default = f a
+  guard_target =ₐ ∀ {α : Type u} [inst : Inhabited α] (a : α) (f : α → α), f a = default → default = f a
   intro α inst a f h
   exact h.symm
 

tests/lean/run/simpLetFunIssue.lean

@@ -4,7 +4,7 @@ example : (λ x => x)
              let_fun foo := λ y => id (id y)
              foo (0 + x)) := by
   simp -zeta only [id]
-  guard_target =ₛ
+  guard_target =ₐ
            (λ x => x)
            =
            (λ x : Nat =>