)]}'
{
  "commit": "358bb770f7609a55ab274bdc6b8faa1af74dbe87",
  "tree": "d543dc8972c8ee8ee9b67c38bcd3d26722a52de3",
  "parents": [
    "86db67c4444ebef438f93b8ded810cd659f4f6f6"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Apr 30 18:53:44 2025 +0200"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Wed Apr 30 18:53:44 2025 +0200"
  },
  "message": "feat: insertMany_append lemmas for map variants\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "6ba7d481467c8dc08d03ae23f92b7ffaa2bc0413",
      "old_mode": 33188,
      "old_path": "src/Std/Data/DHashMap/Lemmas.lean",
      "new_id": "e84b351037767aaa247bab74298d8fac1436b8db",
      "new_mode": 33188,
      "new_path": "src/Std/Data/DHashMap/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "7bc28c2f7d1e7fca717544cc14683b3c2e078532",
      "old_mode": 33188,
      "old_path": "src/Std/Data/DHashMap/RawLemmas.lean",
      "new_id": "cbcbe618e6b34815e3fdc02595fe8bd53baa11bd",
      "new_mode": 33188,
      "new_path": "src/Std/Data/DHashMap/RawLemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "1b2899ebc5cf39e566b8f108fa119f3dbc232acb",
      "old_mode": 33188,
      "old_path": "src/Std/Data/DTreeMap/Lemmas.lean",
      "new_id": "b21dc451735a6027ba55fd46ba82e2cce83702ec",
      "new_mode": 33188,
      "new_path": "src/Std/Data/DTreeMap/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "e7105807326945599720ccea8ce64535aa78a6f7",
      "old_mode": 33188,
      "old_path": "src/Std/Data/DTreeMap/Raw/Lemmas.lean",
      "new_id": "49ca4fda21d362c0347231381747210516cbacae",
      "new_mode": 33188,
      "new_path": "src/Std/Data/DTreeMap/Raw/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "e00a86c35fc5c7071a17bdb55f12798973e6243a",
      "old_mode": 33188,
      "old_path": "src/Std/Data/ExtDHashMap/Lemmas.lean",
      "new_id": "1c7d99ea24dcaef91dc4e928711bb24bc34af086",
      "new_mode": 33188,
      "new_path": "src/Std/Data/ExtDHashMap/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "5478229af7a740ca424949d427e5f3912bab6596",
      "old_mode": 33188,
      "old_path": "src/Std/Data/ExtHashMap/Lemmas.lean",
      "new_id": "39ec30cb481bce72b5230be0ff3ab7f3e4ace866",
      "new_mode": 33188,
      "new_path": "src/Std/Data/ExtHashMap/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "178efcab54b876645bd0a84bb221bc58d43f67da",
      "old_mode": 33188,
      "old_path": "src/Std/Data/ExtHashSet/Lemmas.lean",
      "new_id": "ad15bbc52cf2808edd437595aa2de1838b07c676",
      "new_mode": 33188,
      "new_path": "src/Std/Data/ExtHashSet/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "e16cd1b179ea68102a53631da829ac6862e484e2",
      "old_mode": 33188,
      "old_path": "src/Std/Data/HashMap/Lemmas.lean",
      "new_id": "eaf9b598ecd25024cc1cc9c46dccd2d4be6fb6ce",
      "new_mode": 33188,
      "new_path": "src/Std/Data/HashMap/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "9dc2564e240a6a0d3b565288879b6c405858c134",
      "old_mode": 33188,
      "old_path": "src/Std/Data/HashMap/RawLemmas.lean",
      "new_id": "ae903f5ab8520ee2feb87d219727e9cc62bc578f",
      "new_mode": 33188,
      "new_path": "src/Std/Data/HashMap/RawLemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "da9ed00492967596ccb91090cae172ba7635cd68",
      "old_mode": 33188,
      "old_path": "src/Std/Data/HashSet/Lemmas.lean",
      "new_id": "ae932fecbcc9d41fb19e8e75c2aa7bcbdb5a93ad",
      "new_mode": 33188,
      "new_path": "src/Std/Data/HashSet/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "4188f5a0f4c1b213d3d977b3ac1310418b0701e3",
      "old_mode": 33188,
      "old_path": "src/Std/Data/HashSet/RawLemmas.lean",
      "new_id": "7f99f504b388ad9437ee6470da010a1929481503",
      "new_mode": 33188,
      "new_path": "src/Std/Data/HashSet/RawLemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "bea3fed741c0fc77c23cfd8067a143eec19d663f",
      "old_mode": 33188,
      "old_path": "src/Std/Data/TreeMap/Lemmas.lean",
      "new_id": "8226397a1b2cdca15c31e8ded6cd0bf6baf34939",
      "new_mode": 33188,
      "new_path": "src/Std/Data/TreeMap/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "8f1747c0c5f0c4baad5a217caa668d31a254bb06",
      "old_mode": 33188,
      "old_path": "src/Std/Data/TreeMap/Raw/Lemmas.lean",
      "new_id": "0ae99901219d60a373fcd162002c3e764421e6b4",
      "new_mode": 33188,
      "new_path": "src/Std/Data/TreeMap/Raw/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "b3d3cc8511e3d7b69afd485e4a2e5b8ccc0a7d12",
      "old_mode": 33188,
      "old_path": "src/Std/Data/TreeSet/Lemmas.lean",
      "new_id": "5a3fe241315d937e79bece8648a47961796b1c18",
      "new_mode": 33188,
      "new_path": "src/Std/Data/TreeSet/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "c7a97897bf90625b2f96f0513b311e5c49011a40",
      "old_mode": 33188,
      "old_path": "src/Std/Data/TreeSet/Raw/Lemmas.lean",
      "new_id": "dffbf3bbc97ed1f399d1645cf22876bb1d42618b",
      "new_mode": 33188,
      "new_path": "src/Std/Data/TreeSet/Raw/Lemmas.lean"
    }
  ]
}