feat: add helper tactic for applying List.sizeOf_lt_of_mem in termination proofs

src/Init/Data/List/BasicAux.lean

@@ -121,6 +121,15 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a <
   | head => simp_arith
   | tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)
 
+macro "sizeOf_list_dec" : tactic =>
+  `(first
+    | apply sizeOf_lt_of_mem; assumption; done
+    | apply Nat.lt_trans (sizeOf_lt_of_mem ?h)
+      case' h => assumption
+      simp_arith)
+
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
+
 theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs = cs := by
   induction as with
   | nil => assumption

tests/lean/run/forInRangeWF.lean

@@ -8,3 +8,17 @@ def Expr.size (e : Expr) : Nat := Id.run do
     for h : i in [: args.size] do
       sz := sz + size (args.get ⟨i, h.upper⟩)
     return sz
+
+namespace Ex2
+inductive Expr where
+  | app (f : String) (args : List Expr)
+
+def Expr.size (e : Expr) : Nat := Id.run do
+  match e with
+  | app f args =>
+    let mut sz := 1
+    for h : arg in args do
+      sz := sz + size arg
+    return sz
+
+end Ex2