doc: warning for wf_preprocess (#10897)

This PR adds a warning to `wf_preproces` that these lemmas can be used
to introduce hidden partiality.

---------

Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>

src/Init/Tactics.lean

@@ -2317,6 +2317,12 @@ Theorems tagged with the `wf_preprocess` attribute are used during the processin
 by well-founded recursion. They are applied to the function's body to add additional hypotheses,
 such as replacing `if c then _ else _` with `if h : c then _ else _` or `xs.map` with
 `xs.attach.map`. Also see `wfParam`.
+
+Warning: These rewrites are only applied to the declaration for the purpose of the logical
+definition, but do not affect the compiled code. In particular they can cause a function definition
+that diverges as compiled to be accepted without an explicit `partial` keyword, for example if they
+remove irrelevant subterms or change the evaluation order by hiding terms under binders. Therefore
+avoid tagging theorems with `[wf_preprocess]` unless they preserve also operational behavior.
 -/
 syntax (name := wf_preprocess) "wf_preprocess" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr