feat: exhaustive offset constraint propagation in the grind tactic

[leodemoura]

This PR implements exhaustive offset constraint propagation in the grind tactic. This enhancement minimizes the number of case splits performed by grind. For instance, it can solve the following example without performing any case splits:

example (p q r s : Prop) (a b : Nat) : (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → a ≤ b → b + 2 ≤ c → p ∧ q ∧ r ∧ s := by
  grind (splits := 0)

TODO: support for equational offset constraints.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 40efbb9b7a5e5e05e7e4009a8287d7228d18552a --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-13 04:41:58)