)]}'
{
  "commit": "62e0cf067af1febf28eee560a43bd4f72d23bfaa",
  "tree": "e1435e25f911aab3be5e7185b1376e8448c311bb",
  "parents": [
    "0fb927cce7d41305b6ee96b51f076cbda9681d17"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Fri Nov 13 23:33:34 2026 +0000"
  },
  "committer": {
    "name": "GitHub",
    "email": "noreply@github.com",
    "time": "Fri Nov 13 23:33:34 2026 +0000"
  },
  "message": "perf: use a custom `contradiction` when proving `match` equations (#16460)\n\nThis PR makes generating the equations of a `match` with many\nalternatives faster when the patterns contain literals nested in\nconstructors, e.g., `| some \"a\" \u003d\u003e ..`. For 32 alternatives of this\nform, generating the `match` equations takes 0.53s instead of 1.45s.\n\nThe equation proofs used the general `contradiction` tactic, which looks\nfor a pair of hypotheses `h₁ : p` and `h₂ : ¬ p` by comparing every\nhypothesis of the form `p → False` with every other hypothesis. The\ngoals of these proofs have one such hypothesis for each alternative, and\nthe tactic is tried on two goals per alternative, so the proof of the\ncatch-all equation was cubic in the number of alternatives. The proofs\nnow use `contradictionForEqns`, which only performs the checks that\nclose these goals: a disequality between definitionally equal terms, a\ngeneralized disequality (`processGenDiseq`), and an element of an empty\ntype.\n\n🤖 Generated with [Claude Code](https://claude.com/claude-code)\n\nCo-authored-by: Claude Fable 5.2 \u003cnoreply@anthropic.com\u003e",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "c23bc5550a7e67b4ee5d435331872850e5301506",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Match/MatchEqs.lean",
      "new_id": "3a6da082c6acbedb018860c5047a9956168c10b2",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Match/MatchEqs.lean"
    },
    {
      "type": "modify",
      "old_id": "3f914bba5bcc034fe4af0efa566324997685cf2e",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Contradiction.lean",
      "new_id": "b4a0718803ae58a2900e023acc6364d131f41703",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Contradiction.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "eb3b0c549a221ab656f7e4d69050f2813c5ddfd8",
      "new_mode": 33188,
      "new_path": "tests/elab/matchEqnsIteTree.lean"
    }
  ]
}