From f9abcae4e4bbdf0864e99129558b3503ea4d8e53 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Sep 2022 19:53:04 -0700
Subject: [PATCH] chore: simplify tactic macro

The `[inlineIfReduce]` at `List.toArrayAux` is currently very
expensive, and this example produces a deep recursion when inlining
the `List.toArrayAux` applications.
---
 tests/lean/run/wfEqnsIssue.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tests/lean/run/wfEqnsIssue.lean b/tests/lean/run/wfEqnsIssue.lean
index f101a29f2b..1f74010b00 100644
--- a/tests/lean/run/wfEqnsIssue.lean
+++ b/tests/lean/run/wfEqnsIssue.lean
@@ -62,8 +62,7 @@ theorem Nat.le_add_right_of_le (n m : Nat) : n ≤ m → n ≤ m + k :=
 macro_rules
 | `(tactic| decreasing_tactic) =>
  `(tactic|
-   (simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]
-    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
+   (simp_wf
     repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
     simp [Nat.add_comm (n := 1), Nat.succ_add, Nat.mul_succ]
     try apply Nat.lt_succ_of_le