Update tests/lean/guessLexTricky.lean

src/Init/Data/Nat/Basic.lean

@@ -278,7 +278,7 @@ theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
 
-@[simp] theorem pred_le : ∀ (n : Nat), pred n ≤ n
+theorem pred_le : ∀ (n : Nat), pred n ≤ n
   | zero   => Nat.le.refl
   | succ _ => le_succ _
 
@@ -288,7 +288,7 @@ theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
 
 theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt
 
-theorem sub_le (n m : Nat) : n - m ≤ n := by
+@[simp] theorem sub_le (n m : Nat) : n - m ≤ n := by
   induction m with
   | zero      => exact Nat.le_refl (n - 0)
   | succ m ih => apply Nat.le_trans (pred_le (n - m)) ih

tests/lean/guessLexTricky.lean

@@ -39,24 +39,28 @@ macro_rules | `(tactic|search_lex $ts:tacticSeq) => `(tactic| (
 mutual
 def prod (x y z : Nat) : Nat :=
   if y % 2 = 0 then eprod x y z else oprod x y z
+-- termination_by (y, 1, 0)
 decreasing_by
-  -- TODO: Why does it not work to wrap it all in `all_goals`?
-  all_goals simp_wf
-  · search_lex solve
-      | decreasing_trivial
-      | apply Nat.bitwise_rec_lemma; assumption
-  · search_lex solve
+  all_goals
+    simp_wf
+    search_lex solve
       | decreasing_trivial
       | apply Nat.bitwise_rec_lemma; assumption
 
 def oprod (x y z : Nat) := eprod x (y - 1) (z + x)
+-- termination_by (y, 0, 1)
 decreasing_by
   simp_wf
-  search_lex solve
-    | decreasing_trivial
-    | apply Nat.bitwise_rec_lemma; assumption
+  try -- the need for `try` here is fishy
+      -- the proof with explicit `termination_by` does not need it, so it should not throw
+      -- GuessLex off, but without `try` it does
+      -- This appeared after #4522, which made Nat.sub_le a simp lemma
+    search_lex solve
+      | decreasing_trivial
+      | apply Nat.bitwise_rec_lemma; assumption
 
 def eprod (x y z : Nat) := if y = 0 then z else prod (2 * x) (y / 2) z
+-- termination_by (y, 0, 0)
 decreasing_by
   simp_wf
   search_lex solve
@@ -64,7 +68,3 @@ decreasing_by
     | apply Nat.bitwise_rec_lemma; assumption
 
 end
--- termination_by
---   prod x y z => (y, 2)
---   oprod x y z => (y, 1)
---   eprod x y z => (y, 0)