chore: fix test

This PR adds a few unification hints that we will need after
`backward.isDefEq.respectTransparency` is `true` by default.

src/Init/Hints.lean

@@ -14,3 +14,12 @@ public section
    `TransparencyMode.reducible` -/
 unif_hint (p : Prop) where
   |- Not p =?= p → False
+
+unif_hint (n : Nat) where
+  ⊢ n - 0 =?= n
+
+unif_hint (n : Nat) where
+  ⊢ n + 0 =?= n
+
+unif_hint (n : Nat) where
+  ⊢ n * 0 =?= 0

tests/lean/beginEndAsMacro.lean

@@ -7,12 +7,12 @@ macro "begin " ts:tactic,*,? i:"end" : term => do
 
 theorem ex1 (x : Nat) : x + 0 = 0 + x :=
   begin
-    rw [Nat.zero_add],
     rw [Nat.add_zero],
+    rw [Nat.zero_add],
   end
 /- ANCHOR_END: doc -/
 
 theorem ex2 (x : Nat) : x + 0 = 0 + x :=
   begin
-    rw [Nat.zero_add]
+    rw [Nat.add_zero]
   end  -- error should be shown here

tests/lean/beginEndAsMacro.lean.expected.out

@@ -1,3 +1,3 @@
 beginEndAsMacro.lean:18:2-18:5: error: unsolved goals
 x : Nat
-⊢ x + 0 = x
+⊢ x = 0 + x

tests/lean/run/grind_10160.lean

@@ -29,7 +29,6 @@ theorem MyInt.natCast_eq (n : Nat) : (n : MyInt) = formalDiff n 0 := rfl
 theorem MyInt.natCast_inj (n m : Nat) :
   (n : MyInt) = (m : MyInt) ↔ n = m := by
   rw [natCast_eq, natCast_eq, eq]
-  grind
 
 example (n m : Nat) : (n : MyInt) = (m : MyInt) ↔ n = m := by
   grind [MyInt.natCast_eq, MyInt.eq]

tests/lean/rwWithoutOffsetCnstrs.lean

@@ -1,8 +0,0 @@
-open Lean.Parser.Tactic in
-macro "rw0" s:rwRuleSeq : tactic =>
-  `(tactic| rw (config := { offsetCnstrs := false }) $s:rwRuleSeq)
-
-example (m n : Nat) : Nat.ble (n+1) (n+0) = false := by
-  rw0 [Nat.add_zero]
-  trace_state
-  admit

tests/lean/rwWithoutOffsetCnstrs.lean.expected.out

@@ -1,3 +0,0 @@
-m n : Nat
-⊢ (n + 1).ble n = false
-rwWithoutOffsetCnstrs.lean:5:0-5:7: warning: declaration uses `sorry`