)]}'
{
  "commit": "19202bc2450f0b240a4ad6431abe4b690455a92c",
  "tree": "5b178804eeb85a00edd133031df36fcfa8e6d3c4",
  "parents": [
    "bbf92e1a55fd46bb109063ed40abea4bdf631ffd"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Nov 02 03:11:42 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Mon Nov 02 03:11:42 2026 +0000"
  },
  "message": "feat: push Nat and Int casts through arithmetic in the Sym.Arith normalizer\n\nThis PR makes the `Sym.Arith` normalizer push `Nat` and `Int` casts through `+`, `*` and powers with a literal exponent, and for `Int` also through `-`, negation and casts from `Nat`. As a result, `(m + n) • x \u003d m • x + n • x` and `((m * n : Nat) : R) \u003d ((n * m : Nat) : R)` are now proved by `Sym.simp` with `arith`, and by the `grind` normalizer. Truncated `Nat` subtraction, division and remainder are still treated as atoms.\n\nEach push is one step with the existing `Grind.Semiring.natCast_*` and `Grind.Ring.intCast_*` lemmas, applied only when the cast instance and the inner operator\u0027s instance are canonical. A cast at the root is normalized too. In a noncommutative structure, the cast\u0027s argument is first normalized in `Nat`/`Int`: casts are central, but the normal form there does not reorder them.\n\nCloses #15502\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "2c372e64e3359bd9f2e9b1b32ed323a7b898f0db",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Sym/Arith/Norm.lean",
      "new_id": "4ca0ada86aadc4db0479f6202fd740bee2e89e8a",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Sym/Arith/Norm.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "25a0203ca9505fe398d2bc2bb284c0281b5e6074",
      "new_mode": 33188,
      "new_path": "tests/elab/sym_arith_norm_cast.lean"
    }
  ]
}