feat: add wf_preprocess theorems for List.any

Author: jcreedcmu

src/Init/Data/List/Attach.lean

@@ -867,4 +867,13 @@ and simplifies these to the function directly taking the value.
       binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
   simp [wfParam]
 
+@[wf_preprocess] theorem any_wfParam {xs : List α} {f : α → Bool} :
+    (wfParam xs).any f = xs.attach.unattach.any f := by
+  simp [wfParam]
+
+@[wf_preprocess] theorem any_unattach {P : α → Prop} {xs : List (Subtype P)} {f : α → Bool} :
+    xs.unattach.any f = xs.any fun ⟨x, h⟩ =>
+      binderNameHint x f <| binderNameHint h () <| f (wfParam x) := by
+  simp [wfParam]
+
 end List

tests/lean/run/wf_preprocess.lean

@@ -361,4 +361,12 @@ theorem Tree.map2.eq_1.{u_1, u_2, u_3} : ∀ {α : Type u_1} {β : Type u_2} {γ
 #guard_msgs in
 #print equations Tree.map2
 
+#guard_msgs in
+def Tree.any (f : α → Bool) (t : Tree α) : Bool :=
+  if f t.val
+  then true
+  else t.cs.any fun c => any f c
+termination_by t
+decreasing_by cases t; decreasing_tactic
+
 end Binary