chore: omega to lia replacements that require unfolding min/max

[chenson2018]

This is a draft PR, as we may not want to actually take this approach. This is mostly to point out where this pattern applies.

#40015 was merged with some outstanding comments from @grunweg, asking about some replacements of omega with grind made in that PR. In general this is undesirable, as we would rather replace with lia for the purposes of more clearly communicating the intent of the proof and potential performance benefits.

I noted that in the couple of cases there, all that was required to use lia was some unfolding. I had a guess that this would be the case throughout Mathlib, and decided to check this against #nightly-testing-mathlib>nightly-testing regression log, which records all places that omega cannot be directly replaced with lia. There are only 44 places this happens, and about 75% of them amount to using max_def/min_def as shown in this PR.

---

[github-actions]

PR summary aa66269d4b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit aa66269d4b
Reference commit e577c1669e

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).