diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean
index 08b7e4f5f5..e328784cca 100644
--- a/src/Init/WFTactics.lean
+++ b/src/Init/WFTactics.lean
@@ -9,18 +9,22 @@ import Init.WF
 
 macro "simp_wf" : tactic => `(simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
+syntax "decreasing_tactic_trivial" : tactic -- Extensible helper tactic for `decreasing_tactic`
+
+macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| simp (config := { arith := true }); done)
+macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| assumption)
+macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
+macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i
+macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| apply Nat.pred_lt; assumption)  -- i-1 < i if i ≠ 0
+macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| decide) -- e.g., 0 < 1
+macro_rules | `(tactic| decreasing_tactic_trivial) => `(tactic| apply Nat.lt_succ_self) -- i < i+1
+
 macro "decreasing_tactic" : tactic =>
  `((simp_wf
     repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
     repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
     first
-    | apply Nat.lt_succ_self                   -- i < i+1
-    | decide                                   -- e.g., 0 < 1
-    | apply Nat.pred_lt; assumption            -- i-1 < i if i ≠ 0
-    | apply Nat.pred_lt'; assumption           -- i-1 < i if j < i
-    | apply Nat.sub_succ_lt_self; assumption   -- a - (i+1) < a - i if i < a
-    | assumption
-    | simp (config := { arith := true }); done
+    | decreasing_tactic_trivial
     | fail "failed to prove termination, possible solutions:\n  - Use `have`-expressions to prove the remaining goals\n  - Use `termination_by` to specify a different well-founded relation\n  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal"
     -- TODO: linearith
     -- TODO: improve