)]}'
{
  "commit": "1a61b025fe21be953a5554c60ed1389bd58c5a8a",
  "tree": "85d65083207d618ba1f760a0bde6851b97664ee9",
  "parents": [
    "584ed5f33e8beec04277a6255b8902019213e927"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Fri Aug 22 21:34:31 2025 +1000"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Fri Aug 22 21:34:31 2025 +1000"
  },
  "message": "feat: theorems about Nat/Int/Rat needed for dyadics\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "947a95f7000e4a9a03f35a592cde4cdc40c9f20a",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Int/Bitwise/Basic.lean",
      "new_id": "749592645c04fe66cc8f44dbe9be573f18a9b5b3",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Int/Bitwise/Basic.lean"
    },
    {
      "type": "modify",
      "old_id": "cc959d5a581444613fac0e864c1151b7f4dfad15",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Int/Bitwise/Lemmas.lean",
      "new_id": "ae3b94a351299f44dc0c88ed0244e90f8c782568",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Int/Bitwise/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "1c7a4f428e587814052a755479b79869d4965953",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Int/Pow.lean",
      "new_id": "e7cc4d86ec8ed4efac51b3e91d5ceac82b4942db",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Int/Pow.lean"
    },
    {
      "type": "modify",
      "old_id": "3a3b7519bd3ef7b333aa9ce9dd4a9ff1d3cd9e74",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Nat/Lemmas.lean",
      "new_id": "80f80004102e19f9f339798251dc6c51df117c52",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Nat/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "aa23360a047eede02762526355f705788e511856",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Rat/Lemmas.lean",
      "new_id": "6dd9ae8b938cc049691dac51e93f22b0123e0771",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Rat/Lemmas.lean"
    }
  ]
}