)]}'
{
  "commit": "19b147211cf719f3f72842b31d2fb49a69e75807",
  "tree": "493ccc6e1eb4caba044efa46d6b9db0cd4f497fa",
  "parents": [
    "187f7515b53201b2bcfe93f757a48b8e88a564b2"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Nov 07 06:58:31 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sat Nov 07 06:58:31 2026 +0000"
  },
  "message": "fix: keep `Nat.reduceSubDiff` off where `Init.Data.Nat.Simproc` is not imported\n\nThe `pn \u003d nn` cases of `Nat.reduceSubDiff` used `Nat.add_sub_cancel` and `Nat.add_sub_add_right`, which are available in modules that do not import `Init.Data.Nat.Simproc`. Since a simproc case fires only if its lemma is in the environment, the simproc started firing in those stdlib modules, breaking `List.set_append` once stage0 is updated. This commit uses copies in `Nat.Simproc`, restoring the previous behavior.\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "186b301e0ed68bff3bba6e1525e54812a0eccb1b",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Nat/Simproc.lean",
      "new_id": "26cca3ca9cbbd8402419b126715ca4a7c27854c6",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Nat/Simproc.lean"
    },
    {
      "type": "modify",
      "old_id": "ad86cfc528556b23e8a2a3bd53ee873cdcfadb59",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean",
      "new_id": "e67ebeae11e714c27c3f0123866ff04ec784cbc1",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean"
    }
  ]
}