minor fix

lean-dojo · Mar 15, 2024 · 929923e · 929923e
1 parent 021dbcc
commit 929923e
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 62 deletions.
diff --git a/scripts/generate-benchmark-lean4.ipynb b/scripts/generate-benchmark-lean4.ipynb
@@ -359,26 +359,26 @@
      "name": "stderr",
      "output_type": "stream",
      "text": [
-      "\u001b[32m2024-03-13 19:47:41.611\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m116\u001b[0m - \u001b[1mLoading the traced repo from /Users/yangky/.cache/lean_dojo/leanprover-community-mathlib4-3c307701fa7e9acbdc0680d7f3b9c9fed9081740/mathlib4\u001b[0m\n",
-      "2024-03-13 19:47:45,594\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
-      "100%|██████████| 5042/5042 [33:51<00:00,  2.48it/s]   \n",
-      "\u001b[32m2024-03-13 20:21:47.931\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='a751d21d4b68c999accb6fc5d960538af26ad5ec') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:22:12.544\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:22:24.246\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77') relies on an unsupported Lean version: 8fc1af650ad6d31cf766d9bc84119149330e7d4e\u001b[0m\n",
+      "\u001b[32m2024-03-14 19:43:28.334\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36mlean_dojo.data_extraction.trace\u001b[0m:\u001b[36mtrace\u001b[0m:\u001b[36m116\u001b[0m - \u001b[1mLoading the traced repo from /Users/yangky/.cache/lean_dojo/leanprover-community-mathlib4-3c307701fa7e9acbdc0680d7f3b9c9fed9081740/mathlib4\u001b[0m\n",
+      "2024-03-14 19:43:30,651\tINFO worker.py:1715 -- Started a local Ray instance. View the dashboard at \u001b[1m\u001b[32m127.0.0.1:8265 \u001b[39m\u001b[22m\n",
+      "100%|██████████| 5042/5042 [12:52<00:00,  6.53it/s]  \n",
+      "\u001b[32m2024-03-14 19:56:33.430\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='a751d21d4b68c999accb6fc5d960538af26ad5ec') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n",
+      "\u001b[32m2024-03-14 19:56:48.006\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/leanprover/lean4-cli', commit='be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5') relies on an unsupported Lean version: ec941735c80dc54c53948e30c428905b6600f95a\u001b[0m\n",
+      "\u001b[32m2024-03-14 19:56:57.443\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/xubaiw/CMark.lean', commit='0077cbbaa92abf855fc1c0413e158ffd8195ec77') relies on an unsupported Lean version: 8fc1af650ad6d31cf766d9bc84119149330e7d4e\u001b[0m\n",
       "Following Github server redirection from /repos/mhuisi/lean4-cli to /repositories/341363356\n",
-      "\u001b[32m2024-03-13 20:22:28.176\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa') relies on an unsupported Lean version: 216d2460e0adec8317fdeeb6f2543cb7442564fd\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:22:34.689\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='280d75fdfe7be8eb337be7f1bf8479b4aac09f71') relies on an unsupported Lean version: 0d7051497ea09b2b4a4ef608e371b8f317487c3c\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:22:38.724\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1') relies on an unsupported Lean version: f6cd6c069587cfe62dd68cb6330f9ad794a56724\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:27:56.583\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m6\u001b[0m - \u001b[1m106446 theorems in total\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:27:56.636\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:27:56.682\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:34:56.016\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m102446 theorems and 211202 tactics saved to ../leandojo_benchmark_4/random/train.json\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:34:59.491\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 4010 tactics saved to ../leandojo_benchmark_4/random/val.json\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:35:01.427\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 4579 tactics saved to ../leandojo_benchmark_4/random/test.json\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:35:34.575\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m102446 theorems and 208396 tactics saved to ../leandojo_benchmark_4/novel_premises/train.json\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:35:37.140\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 5742 tactics saved to ../leandojo_benchmark_4/novel_premises/val.json\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:35:37.888\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 5653 tactics saved to ../leandojo_benchmark_4/novel_premises/test.json\u001b[0m\n",
-      "\u001b[32m2024-03-13 20:36:37.996\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m73\u001b[0m - \u001b[1m158266 theorems/definitions from 5042 files saved to ../leandojo_benchmark_4/corpus.jsonl\u001b[0m\n"
+      "\u001b[32m2024-03-14 19:57:00.938\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/mhuisi/lean4-cli', commit='39229f3630d734af7d9cfb5937ddc6b41d3aa6aa') relies on an unsupported Lean version: 216d2460e0adec8317fdeeb6f2543cb7442564fd\u001b[0m\n",
+      "\u001b[32m2024-03-14 19:57:07.628\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/fgdorais/lean4-unicode-basic', commit='280d75fdfe7be8eb337be7f1bf8479b4aac09f71') relies on an unsupported Lean version: 0d7051497ea09b2b4a4ef608e371b8f317487c3c\u001b[0m\n",
+      "\u001b[32m2024-03-14 19:57:11.601\u001b[0m | \u001b[33m\u001b[1mWARNING \u001b[0m | \u001b[36mlean_dojo.data_extraction.lean\u001b[0m:\u001b[36m__post_init__\u001b[0m:\u001b[36m449\u001b[0m - \u001b[33m\u001b[1mLeanGitRepo(url='https://github.com/hargonix/LeanInk', commit='2447df5cc6e48eb965c3c3fba87e46d353b5e9f1') relies on an unsupported Lean version: f6cd6c069587cfe62dd68cb6330f9ad794a56724\u001b[0m\n",
+      "\u001b[32m2024-03-14 19:59:59.133\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_data\u001b[0m:\u001b[36m6\u001b[0m - \u001b[1m116695 theorems in total\u001b[0m\n",
+      "\u001b[32m2024-03-14 19:59:59.168\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_randomly\u001b[0m:\u001b[36m18\u001b[0m - \u001b[1mSplitting the theorems randomly\u001b[0m\n",
+      "\u001b[32m2024-03-14 19:59:59.211\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36msplit_by_premise\u001b[0m:\u001b[36m8\u001b[0m - \u001b[1mSplitting the theorems by premises\u001b[0m\n",
+      "\u001b[32m2024-03-14 20:02:16.104\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m112695 theorems and 234380 tactics saved to ../leandojo_benchmark_4/random/train.json\u001b[0m\n",
+      "\u001b[32m2024-03-14 20:02:21.292\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 4116 tactics saved to ../leandojo_benchmark_4/random/val.json\u001b[0m\n",
+      "\u001b[32m2024-03-14 20:02:24.068\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 3792 tactics saved to ../leandojo_benchmark_4/random/test.json\u001b[0m\n",
+      "\u001b[32m2024-03-14 20:03:40.016\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m111570 theorems and 229668 tactics saved to ../leandojo_benchmark_4/novel_premises/train.json\u001b[0m\n",
+      "\u001b[32m2024-03-14 20:03:45.758\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 5779 tactics saved to ../leandojo_benchmark_4/novel_premises/val.json\u001b[0m\n",
+      "\u001b[32m2024-03-14 20:03:47.246\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_proofs\u001b[0m:\u001b[36m49\u001b[0m - \u001b[1m2000 theorems and 5573 tactics saved to ../leandojo_benchmark_4/novel_premises/test.json\u001b[0m\n",
+      "\u001b[32m2024-03-14 20:05:22.288\u001b[0m | \u001b[1mINFO    \u001b[0m | \u001b[36m__main__\u001b[0m:\u001b[36mexport_premises\u001b[0m:\u001b[36m73\u001b[0m - \u001b[1m158266 theorems/definitions from 5042 files saved to ../leandojo_benchmark_4/corpus.jsonl\u001b[0m\n"
      ]
     }
    ],
@@ -438,13 +438,6 @@
      "text": [
       "    5042\n"
      ]
-    },
-    {
-     "name": "stderr",
-     "output_type": "stream",
-     "text": [
-      "python(38298) MallocStackLogging: can't turn off malloc stack logging because it was not enabled.\n"
-     ]
     }
    ],
    "source": [
@@ -500,13 +493,8 @@
     {
      "data": {
       "text/plain": [
-       "('Mathlib/Data/MvPolynomial/Equiv.lean',\n",
+       "('Mathlib/Data/MvPolynomial/CommRing.lean',\n",
        " ['Mathlib/Data/MvPolynomial/Variables.lean',\n",
-       "  'Mathlib/Data/Polynomial/AlgebraMap.lean',\n",
-       "  'Mathlib/Data/MvPolynomial/Rename.lean',\n",
-       "  'Mathlib/Logic/Equiv/Fin.lean',\n",
-       "  'Mathlib/Algebra/BigOperators/Fin.lean',\n",
-       "  'Mathlib/Data/Finsupp/Fin.lean',\n",
        "  '.lake/packages/lean4/src/lean/Init.lean'])"
       ]
      },
@@ -528,7 +516,7 @@
     {
      "data": {
       "text/plain": [
-       "40"
+       "23"
       ]
      },
      "execution_count": 11,
@@ -557,11 +545,11 @@
     {
      "data": {
       "text/plain": [
-       "{'full_name': 'MvPolynomial.pUnitAlgEquiv',\n",
-       " 'code': \"@[simps]\\ndef pUnitAlgEquiv : MvPolynomial PUnit R ≃ₐ[R] R[X] where\\n  toFun := eval₂ Polynomial.C fun _ => Polynomial.X\\n  invFun := Polynomial.eval₂ MvPolynomial.C (X PUnit.unit)\\n  left_inv := by\\n    let f : R[X] →+* MvPolynomial PUnit R := Polynomial.eval₂RingHom MvPolynomial.C (X PUnit.unit)\\n    let g : MvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun _ => Polynomial.X\\n    show ∀ p, f.comp g p = p\\n    apply is_id\\n    · ext a\\n      dsimp\\n      rw [eval₂_C, Polynomial.eval₂_C]\\n    · rintro ⟨⟩\\n      dsimp\\n      rw [eval₂_X, Polynomial.eval₂_X]\\n  right_inv p :=\\n    Polynomial.induction_on p (fun a => by rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C])\\n    (fun p q hp hq => by rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]) fun p n _ => by\\n      rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,\\n        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]\\n  map_mul' _ _ := eval₂_mul _ _\\n  map_add' _ _ := eval₂_add _ _\\n  commutes' _ := eval₂_C _ _ _\",\n",
-       " 'start': [61, 1],\n",
-       " 'end': [86, 31],\n",
-       " 'kind': 'commanddeclaration'}"
+       "{'full_name': 'MvPolynomial.instCommRingMvPolynomial',\n",
+       " 'code': 'instance instCommRingMvPolynomial : CommRing (MvPolynomial σ R) :=\\n  AddMonoidAlgebra.commRing',\n",
+       " 'start': [56, 1],\n",
+       " 'end': [57, 28],\n",
+       " 'kind': 'commanddeclaratio'}"
       ]
      },
      "execution_count": 12,
@@ -595,7 +583,7 @@
     {
      "data": {
       "text/plain": [
-       "102446"
+       "112695"
       ]
      },
      "execution_count": 13,
@@ -619,7 +607,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 14,
    "id": "3cc47f7e",
    "metadata": {},
    "outputs": [
@@ -629,7 +617,7 @@
        "dict_keys(['url', 'commit', 'file_path', 'full_name', 'start', 'end', 'traced_tactics'])"
       ]
      },
-     "execution_count": 15,
+     "execution_count": 14,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -643,7 +631,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": 15,
    "id": "3c2c36a7",
    "metadata": {},
    "outputs": [
@@ -652,11 +640,11 @@
       "text/plain": [
        "('https://github.com/leanprover-community/mathlib4',\n",
        " '3c307701fa7e9acbdc0680d7f3b9c9fed9081740',\n",
-       " 'Mathlib/CategoryTheory/Endofunctor/Algebra.lean',\n",
-       " 'CategoryTheory.Endofunctor.Algebra.Initial.right_inv')"
+       " 'Mathlib/Algebra/Group/Pi/Lemmas.lean',\n",
+       " 'Pi.update_eq_div_mul_mulSingle')"
       ]
      },
-     "execution_count": 16,
+     "execution_count": 15,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -675,17 +663,17 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 16,
    "id": "c29987ff",
    "metadata": {},
    "outputs": [
     {
      "data": {
       "text/plain": [
-       "3"
+       "4"
       ]
      },
-     "execution_count": 17,
+     "execution_count": 16,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -711,18 +699,14 @@
     {
      "data": {
       "text/plain": [
-       "{'tactic': 'rw [strInv, ← (h.to ⟨F.obj A.1, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]',\n",
-       " 'annotated_tactic': ['rw [<a>strInv</a>, ← (h.to ⟨F.obj A.1, F.map A.str⟩).<a>h</a>, ← F.map_id, ← F.map_comp]',\n",
-       "  [{'full_name': 'CategoryTheory.Endofunctor.Algebra.Initial.strInv',\n",
-       "    'def_path': 'Mathlib/CategoryTheory/Endofunctor/Algebra.lean',\n",
-       "    'def_pos': [228, 5],\n",
-       "    'def_end_pos': [228, 11]},\n",
-       "   {'full_name': 'CategoryTheory.Endofunctor.Algebra.Hom.h',\n",
-       "    'def_path': 'Mathlib/CategoryTheory/Endofunctor/Algebra.lean',\n",
-       "    'def_pos': [68, 3],\n",
-       "    'def_end_pos': [68, 4]}]],\n",
-       " 'state_before': 'C : Type u\\ninst✝ : Category.{v, u} C\\nF : C ⥤ C\\nA A₀ A₁ A₂ : Algebra F\\nf : A₀ ⟶ A₁\\ng : A₁ ⟶ A₂\\nh : Limits.IsInitial A\\n⊢ A.str ≫ strInv h = 𝟙 (F.toPrefunctor.obj A.a)',\n",
-       " 'state_after': 'C : Type u\\ninst✝ : Category.{v, u} C\\nF : C ⥤ C\\nA A₀ A₁ A₂ : Algebra F\\nf : A₀ ⟶ A₁\\ng : A₁ ⟶ A₂\\nh : Limits.IsInitial A\\n⊢ F.toPrefunctor.map\\n      ((Limits.IsInitial.to h { a := F.toPrefunctor.obj A.a, str := F.toPrefunctor.map A.str }).f ≫ A.str) =\\n    F.toPrefunctor.map (𝟙 A.a)'}"
+       "{'tactic': 'rcases eq_or_ne i j with (rfl | h)',\n",
+       " 'annotated_tactic': ['rcases <a>eq_or_ne</a> i j with (rfl | h)',\n",
+       "  [{'full_name': 'eq_or_ne',\n",
+       "    'def_path': 'Mathlib/Logic/Basic.lean',\n",
+       "    'def_pos': [208, 9],\n",
+       "    'def_end_pos': [208, 17]}]],\n",
+       " 'state_before': 'case h\\nι : Type u_1\\nα : Type u_2\\nI : Type u\\nf : I → Type v\\nx✝ y : (i : I) → f i\\ni j✝ : I\\ninst✝¹ : DecidableEq I\\ninst✝ : (i : I) → Group (f i)\\ng : (i : I) → f i\\nx : f i\\nj : I\\n⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j',\n",
+       " 'state_after': 'case h.inl\\nι : Type u_1\\nα : Type u_2\\nI : Type u\\nf : I → Type v\\nx✝ y : (i : I) → f i\\ni j : I\\ninst✝¹ : DecidableEq I\\ninst✝ : (i : I) → Group (f i)\\ng : (i : I) → f i\\nx : f i\\n⊢ Function.update g i x i = (g / mulSingle i (g i) * mulSingle i x) i\\n\\ncase h.inr\\nι : Type u_1\\nα : Type u_2\\nI : Type u\\nf : I → Type v\\nx✝ y : (i : I) → f i\\ni j✝ : I\\ninst✝¹ : DecidableEq I\\ninst✝ : (i : I) → Group (f i)\\ng : (i : I) → f i\\nx : f i\\nj : I\\nh : i ≠ j\\n⊢ Function.update g i x j = (g / mulSingle i (g i) * mulSingle i x) j'}"
       ]
      },
      "execution_count": 18,
@@ -731,7 +715,7 @@
     }
    ],
    "source": [
-    "proof[\"traced_tactics\"][0]"
+    "proof[\"traced_tactics\"][1]"
    ]
   },
   {

diff --git a/src/lean_dojo/data_extraction/ast.py b/src/lean_dojo/data_extraction/ast.py
@@ -41,7 +41,7 @@ def _kind_to_node_type(cls, kind: str) -> type:
 
     @classmethod
     def kind(cls: type) -> str:
-        return cls.__name__[:-5].lower()
+        return cls.__name__[:-4].lower()
 
     def traverse_preorder(
         self,
@@ -1498,6 +1498,7 @@ def is_potential_premise_lean4(node: Node) -> bool:
     if (isinstance(node, CommandDeclarationNode) and not node.is_example) or type(
         node
     ) in (
+        LemmaNode,
         MathlibTacticLemmaNode,
         LeanElabCommandCommandIrreducibleDefNode,
         StdTacticAliasAliasNode,