Commit 2026-05-30 15:16 56685ea2

chore: respect naming conventions for defs in more meta code (#39949) This PR removes underscores from various metaprogramming defs which were misnamed. Sometimes meta-level tactic API is named to reflect the tactic syntax, and sometimes expressions representing proofs are named with underscores; but both of these are ordinary parts of the API which should respect ordinary naming conventions for defs. Note that this PR also renames a couple of definitions in Mathlib.Tactic.Linarith.NNRealPreprocesser and Mathlib.Tactic.Linarith.Preprocessing to more closely reflect their type (e.g. using ? for Option, get instead of is for computing data; also Proof instead of Prf to avoid the unnecessary abbreviation). These are exempted by the defsWithUnderscore linter due to living in Mathlib.Tactic. (A change to this is explored in #39890, which removes this heuristic.)