)]}'
{
  "commit": "a01968d9a74ba8ab22177f0992dcfaf4816be8f7",
  "tree": "0ff025fa06d95e445b54649b2de4a97c1a4a3f12",
  "parents": [
    "4307c8e6996977beead4bf2b6b936baa3f5caecd"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Oct 20 22:12:35 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Oct 20 22:12:36 2026 +0000"
  },
  "message": "feat: normalize divisibility constraints and tighten bounds modulo divisors in `lia`\n\nThis PR makes `lia` solve goals with large-modulus divisibility constraints, such as `65536 ∣ 10 * x ⊢ 32768 ∣ x`, without a Cooper case split per residue.\n\nConstraints `d ∣ p` are normalized by reducing the coefficients modulo `d` (balanced) after multiplying by the inverse of the leading coefficient when coprime to `d`, so `32768 ∣ 5*x` becomes `32768 ∣ x`. Bound tightening now applies whenever the value of a bound is known modulo a divisor of `d`, generalizing the previous exact-coefficient match.\n\nCo-Authored-By: Claude Fable 5.1 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "0d334c02f4a08736e675863b63740d4791c6e5c7",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Int/Linear.lean",
      "new_id": "59d14b53f32dbb81d105a9453620ef795ce69ba1",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Int/Linear.lean"
    },
    {
      "type": "modify",
      "old_id": "a236938cf0cabd7d8fdc5a85f244d653f3b836e1",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean",
      "new_id": "3c7be981149795e9dedc7125ef84c8c45dd41c20",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean"
    },
    {
      "type": "modify",
      "old_id": "56c676dd391b07a4a2e76592273c59b72a6fc763",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean",
      "new_id": "2c6a9d1b4797df4a0e6a0c19b4b578209b34cc32",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean"
    },
    {
      "type": "modify",
      "old_id": "bfbb5d9926ca8b2afbc0816693ab18fce64d7687",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean",
      "new_id": "b1ade8924525712b6b5aef1f9d013c86b0a4489b",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean"
    },
    {
      "type": "modify",
      "old_id": "b2854b12bee1a7294068806530cae63ea715153a",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean",
      "new_id": "d60c5c5a28e4b1a8f2f60cb01b4247afb5b75551",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean"
    },
    {
      "type": "modify",
      "old_id": "da6580367d516ca21d4248fb58f57d99da3b48df",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_cutsat_div_1.lean",
      "new_id": "3c4fec78314fbfcc1dc61478c80c5d6cbfb6d6b7",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_cutsat_div_1.lean"
    },
    {
      "type": "modify",
      "old_id": "df33f88be1f5480577287023ac75abafb81d3678",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_cutsat_div_1.lean.out.expected",
      "new_id": "10519d4efa1d725f8ddd0c9a649fd04a3bbdb7d5",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_cutsat_div_1.lean.out.expected"
    },
    {
      "type": "modify",
      "old_id": "de04744f9d0b1f4862a280df5c24ed013a1b8fb2",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_cutsat_nat_dvd.lean.out.expected",
      "new_id": "be522e1c3f9c44f513d22ff30197d47932c29149",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_cutsat_nat_dvd.lean.out.expected"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "f1126a3f2695d7c5b7d30364d2a17828c276d1b8",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_lia_dvd_tight.lean"
    }
  ]
}