)]}'
{
  "commit": "1e40623e3e9438444c8844bdf92ae8c7d0b1f548",
  "tree": "b5ad764738199a39d34d424d78817105158b60b8",
  "parents": [
    "0cc4c918008d64269460bdba41fbcd3df8445af6"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Jul 22 10:29:10 2025 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Tue Jul 22 10:31:56 2025 -0700"
  },
  "message": "fix: `mkCongrSimpCore?`\n\nThis PR fixes another issue at the `congr_simp` theorems that was\naffecting Mathlib. Many thanks to Johan Commelin for creating the mwe.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "5d56b9371d26dbd4c3a7aac4a4fd228598d47204",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/CongrTheorems.lean",
      "new_id": "406507b074e2da5f75b8d76cf86d90d5aff0610d",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/CongrTheorems.lean"
    },
    {
      "type": "modify",
      "old_id": "17b0714cfa7029e1d40b359106ab2fb864c55397",
      "old_mode": 33188,
      "old_path": "tests/lean/run/congrSimpBug.lean",
      "new_id": "38d941abb97e33c88d7222b8ef519a74f787a16f",
      "new_mode": 33188,
      "new_path": "tests/lean/run/congrSimpBug.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "dab087d3e64990b13566cdfc968662dd12539d71",
      "new_mode": 33188,
      "new_path": "tests/lean/run/congrSimpMathlibIssue.lean"
    }
  ]
}