data_examples.ipynb

{
 "metadata": {
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.5"
  },
  "orig_nbformat": 2,
  "kernelspec": {
   "name": "python3",
   "display_name": "Python 3.8.5 64-bit (conda)"
  },
  "interpreter": {
   "hash": "44b085c88637170b78eaf0eb2fce20df4b00e5857441b8c0f7fece75f04e5cf9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2,
 "cells": [
  {
   "source": [
    "# The datasets"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "This is a quick look at the datasets generated in this project."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import jsonlines\n",
    "from pathlib import Path\n",
    "\n",
    "import pandas as pd"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "DATA_DIRECTORY = Path(\"./data/\")  # change as necessary"
   ]
  },
  {
   "source": [
    "## The traced data"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "This is the data which was traced by the tracing code and gathered into tables."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "`tactic_instances` includes position data and a unique key for every tactic that was executed and traced (which is not every tactic in the code)"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                   table          key  executed  \\\n",
       "0       tactic_instances  2001:20:2:1      True   \n",
       "1       tactic_instances   2016:4:1:1      True   \n",
       "2       tactic_instances   2010:4:1:1      True   \n",
       "3       tactic_instances   2013:4:1:1      True   \n",
       "4       tactic_instances   2019:4:1:1      True   \n",
       "...                  ...          ...       ...   \n",
       "181606  tactic_instances    74:57:3:2      True   \n",
       "181607  tactic_instances    74:57:3:3      True   \n",
       "181608  tactic_instances    74:30:2:1      True   \n",
       "181609  tactic_instances    74:60:1:1      True   \n",
       "181610  tactic_instances    83:18:1:1      True   \n",
       "\n",
       "                                                 filename  trace_pos_line  \\\n",
       "0                 lean/library/init/meta/interactive.lean            2033   \n",
       "1                 lean/library/init/meta/interactive.lean            2016   \n",
       "2                 lean/library/init/meta/interactive.lean            2010   \n",
       "3                 lean/library/init/meta/interactive.lean            2013   \n",
       "4                 lean/library/init/meta/interactive.lean            2019   \n",
       "...                                                   ...             ...   \n",
       "181606  mathlib/src/category_theory/abelian/projective...              74   \n",
       "181607  mathlib/src/category_theory/abelian/projective...              74   \n",
       "181608  mathlib/src/category_theory/abelian/projective...              74   \n",
       "181609  mathlib/src/category_theory/abelian/projective...              74   \n",
       "181610  mathlib/src/category_theory/abelian/projective...              83   \n",
       "\n",
       "        trace_pos_column  line  column  depth  index       proof        block  \\\n",
       "0                      1  2001      20      2      1  2034:4:1:1  2001:20:2:1   \n",
       "1                      4  2016       4      1      1  2016:4:1:1   2016:4:1:1   \n",
       "2                      4  2010       4      1      1  2010:4:1:1   2010:4:1:1   \n",
       "3                      4  2013       4      1      1  2013:4:1:1   2013:4:1:1   \n",
       "4                      4  2019       4      1      1  2019:4:1:1   2019:4:1:1   \n",
       "...                  ...   ...     ...    ...    ...         ...          ...   \n",
       "181606                57    74      57      3      2   74:60:1:1    74:17:3:1   \n",
       "181607                57    74      57      3      3   74:60:1:1    74:17:3:1   \n",
       "181608                30    74      30      2      1   74:60:1:1    74:30:2:1   \n",
       "181609                60    74      60      1      1   74:60:1:1    74:60:1:1   \n",
       "181610                18    83      18      1      1   83:18:1:1    83:18:1:1   \n",
       "\n",
       "            parent        prev  succeeded  \n",
       "0       2034:4:1:1  2034:4:1:1        1.0  \n",
       "1          0:0:0:0     0:0:0:0        1.0  \n",
       "2          0:0:0:0     0:0:0:0        1.0  \n",
       "3          0:0:0:0     0:0:0:0        1.0  \n",
       "4          0:0:0:0     0:0:0:0        1.0  \n",
       "...            ...         ...        ...  \n",
       "181606   74:30:2:1   74:17:3:1        1.0  \n",
       "181607   74:30:2:1   74:57:3:2        1.0  \n",
       "181608   74:60:1:1   74:60:1:1        1.0  \n",
       "181609     0:0:0:0     0:0:0:0        1.0  \n",
       "181610     0:0:0:0     0:0:0:0        1.0  \n",
       "\n",
       "[181611 rows x 15 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>table</th>\n      <th>key</th>\n      <th>executed</th>\n      <th>filename</th>\n      <th>trace_pos_line</th>\n      <th>trace_pos_column</th>\n      <th>line</th>\n      <th>column</th>\n      <th>depth</th>\n      <th>index</th>\n      <th>proof</th>\n      <th>block</th>\n      <th>parent</th>\n      <th>prev</th>\n      <th>succeeded</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>tactic_instances</td>\n      <td>2001:20:2:1</td>\n      <td>True</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2033</td>\n      <td>1</td>\n      <td>2001</td>\n      <td>20</td>\n      <td>2</td>\n      <td>1</td>\n      <td>2034:4:1:1</td>\n      <td>2001:20:2:1</td>\n      <td>2034:4:1:1</td>\n      <td>2034:4:1:1</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>tactic_instances</td>\n      <td>2016:4:1:1</td>\n      <td>True</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2016</td>\n      <td>4</td>\n      <td>2016</td>\n      <td>4</td>\n      <td>1</td>\n      <td>1</td>\n      <td>2016:4:1:1</td>\n      <td>2016:4:1:1</td>\n      <td>0:0:0:0</td>\n      <td>0:0:0:0</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>tactic_instances</td>\n      <td>2010:4:1:1</td>\n      <td>True</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2010</td>\n      <td>4</td>\n      <td>2010</td>\n      <td>4</td>\n      <td>1</td>\n      <td>1</td>\n      <td>2010:4:1:1</td>\n      <td>2010:4:1:1</td>\n      <td>0:0:0:0</td>\n      <td>0:0:0:0</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>tactic_instances</td>\n      <td>2013:4:1:1</td>\n      <td>True</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2013</td>\n      <td>4</td>\n      <td>2013</td>\n      <td>4</td>\n      <td>1</td>\n      <td>1</td>\n      <td>2013:4:1:1</td>\n      <td>2013:4:1:1</td>\n      <td>0:0:0:0</td>\n      <td>0:0:0:0</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>tactic_instances</td>\n      <td>2019:4:1:1</td>\n      <td>True</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2019</td>\n      <td>4</td>\n      <td>2019</td>\n      <td>4</td>\n      <td>1</td>\n      <td>1</td>\n      <td>2019:4:1:1</td>\n      <td>2019:4:1:1</td>\n      <td>0:0:0:0</td>\n      <td>0:0:0:0</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>181606</th>\n      <td>tactic_instances</td>\n      <td>74:57:3:2</td>\n      <td>True</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>57</td>\n      <td>74</td>\n      <td>57</td>\n      <td>3</td>\n      <td>2</td>\n      <td>74:60:1:1</td>\n      <td>74:17:3:1</td>\n      <td>74:30:2:1</td>\n      <td>74:17:3:1</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>181607</th>\n      <td>tactic_instances</td>\n      <td>74:57:3:3</td>\n      <td>True</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>57</td>\n      <td>74</td>\n      <td>57</td>\n      <td>3</td>\n      <td>3</td>\n      <td>74:60:1:1</td>\n      <td>74:17:3:1</td>\n      <td>74:30:2:1</td>\n      <td>74:57:3:2</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>181608</th>\n      <td>tactic_instances</td>\n      <td>74:30:2:1</td>\n      <td>True</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>30</td>\n      <td>74</td>\n      <td>30</td>\n      <td>2</td>\n      <td>1</td>\n      <td>74:60:1:1</td>\n      <td>74:30:2:1</td>\n      <td>74:60:1:1</td>\n      <td>74:60:1:1</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>181609</th>\n      <td>tactic_instances</td>\n      <td>74:60:1:1</td>\n      <td>True</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>60</td>\n      <td>74</td>\n      <td>60</td>\n      <td>1</td>\n      <td>1</td>\n      <td>74:60:1:1</td>\n      <td>74:60:1:1</td>\n      <td>0:0:0:0</td>\n      <td>0:0:0:0</td>\n      <td>1.0</td>\n    </tr>\n    <tr>\n      <th>181610</th>\n      <td>tactic_instances</td>\n      <td>83:18:1:1</td>\n      <td>True</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>83</td>\n      <td>18</td>\n      <td>83</td>\n      <td>18</td>\n      <td>1</td>\n      <td>1</td>\n      <td>83:18:1:1</td>\n      <td>83:18:1:1</td>\n      <td>0:0:0:0</td>\n      <td>0:0:0:0</td>\n      <td>1.0</td>\n    </tr>\n  </tbody>\n</table>\n<p>181611 rows × 15 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 3
    }
   ],
   "source": [
    "tactic_instances = pd.read_json(\n",
    "    DATA_DIRECTORY / \"raw_traced_data\" / \"tactic_instances.jsonl\",\n",
    "    orient=\"records\",\n",
    "    lines=True \n",
    ")\n",
    "tactic_instances"
   ]
  },
  {
   "source": [
    "`tactic_state.json` includes basic tactic state information both before and after the tactic executes (again, only for recorded tactics which are a subset of all tactics in the code).  This can be added to."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "               table                 key tactic_instance  \\\n",
       "0       tactic_state  2001:20:2:1:before     2001:20:2:1   \n",
       "1       tactic_state   2001:20:2:1:after     2001:20:2:1   \n",
       "2       tactic_state   2016:4:1:1:before      2016:4:1:1   \n",
       "3       tactic_state    2016:4:1:1:after      2016:4:1:1   \n",
       "4       tactic_state   2010:4:1:1:before      2010:4:1:1   \n",
       "...              ...                 ...             ...   \n",
       "362445  tactic_state     74:30:2:1:after       74:30:2:1   \n",
       "362446  tactic_state    74:60:1:1:before       74:60:1:1   \n",
       "362447  tactic_state     74:60:1:1:after       74:60:1:1   \n",
       "362448  tactic_state    83:18:1:1:before       83:18:1:1   \n",
       "362449  tactic_state     83:18:1:1:after       83:18:1:1   \n",
       "\n",
       "                                                 filename  trace_pos_line  \\\n",
       "0                 lean/library/init/meta/interactive.lean            2033   \n",
       "1                 lean/library/init/meta/interactive.lean            2033   \n",
       "2                 lean/library/init/meta/interactive.lean            2016   \n",
       "3                 lean/library/init/meta/interactive.lean            2016   \n",
       "4                 lean/library/init/meta/interactive.lean            2010   \n",
       "...                                                   ...             ...   \n",
       "362445  mathlib/src/category_theory/abelian/projective...              74   \n",
       "362446  mathlib/src/category_theory/abelian/projective...              74   \n",
       "362447  mathlib/src/category_theory/abelian/projective...              74   \n",
       "362448  mathlib/src/category_theory/abelian/projective...              83   \n",
       "362449  mathlib/src/category_theory/abelian/projective...              83   \n",
       "\n",
       "        trace_pos_column before_after  env_fingerprint  \\\n",
       "0                      1       before     3.935797e+18   \n",
       "1                      1        after     3.935797e+18   \n",
       "2                      4       before     3.935797e+18   \n",
       "3                      4        after     3.935797e+18   \n",
       "4                      4       before     3.935797e+18   \n",
       "...                  ...          ...              ...   \n",
       "362445                30        after     1.800850e+19   \n",
       "362446                60       before     1.800850e+19   \n",
       "362447                60        after     1.800850e+19   \n",
       "362448                18       before     1.769972e+19   \n",
       "362449                18        after     1.769972e+19   \n",
       "\n",
       "                                                decl_name  \\\n",
       "0                                        list.cons.inj_eq   \n",
       "1                                        list.cons.inj_eq   \n",
       "2                                         psum.inl.inj_eq   \n",
       "3                                         psum.inl.inj_eq   \n",
       "4                                          sum.inl.inj_eq   \n",
       "...                                                   ...   \n",
       "362445            category_theory.ProjectiveResolution.of   \n",
       "362446            category_theory.ProjectiveResolution.of   \n",
       "362447            category_theory.ProjectiveResolution.of   \n",
       "362448  category_theory.ProjectiveResolution.category_...   \n",
       "362449  category_theory.ProjectiveResolution.category_...   \n",
       "\n",
       "                                          open_namespaces  goal_count  \n",
       "0       `interactive `expr `tactic `tactic.interactive...           1  \n",
       "1       `interactive `expr `tactic `tactic.interactive...           1  \n",
       "2       `interactive `expr `tactic `tactic.interactive...           1  \n",
       "3       `interactive `expr `tactic `tactic.interactive...           0  \n",
       "4       `interactive `expr `tactic `tactic.interactive...           1  \n",
       "...                                                   ...         ...  \n",
       "362445  `category_theory.ProjectiveResolution `categor...           0  \n",
       "362446  `category_theory.ProjectiveResolution `categor...           1  \n",
       "362447  `category_theory.ProjectiveResolution `categor...           0  \n",
       "362448  `category_theory.ProjectiveResolution `categor...           1  \n",
       "362449  `category_theory.ProjectiveResolution `categor...           0  \n",
       "\n",
       "[362450 rows x 11 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>table</th>\n      <th>key</th>\n      <th>tactic_instance</th>\n      <th>filename</th>\n      <th>trace_pos_line</th>\n      <th>trace_pos_column</th>\n      <th>before_after</th>\n      <th>env_fingerprint</th>\n      <th>decl_name</th>\n      <th>open_namespaces</th>\n      <th>goal_count</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>tactic_state</td>\n      <td>2001:20:2:1:before</td>\n      <td>2001:20:2:1</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2033</td>\n      <td>1</td>\n      <td>before</td>\n      <td>3.935797e+18</td>\n      <td>list.cons.inj_eq</td>\n      <td>`interactive `expr `tactic `tactic.interactive...</td>\n      <td>1</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>tactic_state</td>\n      <td>2001:20:2:1:after</td>\n      <td>2001:20:2:1</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2033</td>\n      <td>1</td>\n      <td>after</td>\n      <td>3.935797e+18</td>\n      <td>list.cons.inj_eq</td>\n      <td>`interactive `expr `tactic `tactic.interactive...</td>\n      <td>1</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>tactic_state</td>\n      <td>2016:4:1:1:before</td>\n      <td>2016:4:1:1</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2016</td>\n      <td>4</td>\n      <td>before</td>\n      <td>3.935797e+18</td>\n      <td>psum.inl.inj_eq</td>\n      <td>`interactive `expr `tactic `tactic.interactive...</td>\n      <td>1</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>tactic_state</td>\n      <td>2016:4:1:1:after</td>\n      <td>2016:4:1:1</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2016</td>\n      <td>4</td>\n      <td>after</td>\n      <td>3.935797e+18</td>\n      <td>psum.inl.inj_eq</td>\n      <td>`interactive `expr `tactic `tactic.interactive...</td>\n      <td>0</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>tactic_state</td>\n      <td>2010:4:1:1:before</td>\n      <td>2010:4:1:1</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2010</td>\n      <td>4</td>\n      <td>before</td>\n      <td>3.935797e+18</td>\n      <td>sum.inl.inj_eq</td>\n      <td>`interactive `expr `tactic `tactic.interactive...</td>\n      <td>1</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>362445</th>\n      <td>tactic_state</td>\n      <td>74:30:2:1:after</td>\n      <td>74:30:2:1</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>30</td>\n      <td>after</td>\n      <td>1.800850e+19</td>\n      <td>category_theory.ProjectiveResolution.of</td>\n      <td>`category_theory.ProjectiveResolution `categor...</td>\n      <td>0</td>\n    </tr>\n    <tr>\n      <th>362446</th>\n      <td>tactic_state</td>\n      <td>74:60:1:1:before</td>\n      <td>74:60:1:1</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>60</td>\n      <td>before</td>\n      <td>1.800850e+19</td>\n      <td>category_theory.ProjectiveResolution.of</td>\n      <td>`category_theory.ProjectiveResolution `categor...</td>\n      <td>1</td>\n    </tr>\n    <tr>\n      <th>362447</th>\n      <td>tactic_state</td>\n      <td>74:60:1:1:after</td>\n      <td>74:60:1:1</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>60</td>\n      <td>after</td>\n      <td>1.800850e+19</td>\n      <td>category_theory.ProjectiveResolution.of</td>\n      <td>`category_theory.ProjectiveResolution `categor...</td>\n      <td>0</td>\n    </tr>\n    <tr>\n      <th>362448</th>\n      <td>tactic_state</td>\n      <td>83:18:1:1:before</td>\n      <td>83:18:1:1</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>83</td>\n      <td>18</td>\n      <td>before</td>\n      <td>1.769972e+19</td>\n      <td>category_theory.ProjectiveResolution.category_...</td>\n      <td>`category_theory.ProjectiveResolution `categor...</td>\n      <td>1</td>\n    </tr>\n    <tr>\n      <th>362449</th>\n      <td>tactic_state</td>\n      <td>83:18:1:1:after</td>\n      <td>83:18:1:1</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>83</td>\n      <td>18</td>\n      <td>after</td>\n      <td>1.769972e+19</td>\n      <td>category_theory.ProjectiveResolution.category_...</td>\n      <td>`category_theory.ProjectiveResolution `categor...</td>\n      <td>0</td>\n    </tr>\n  </tbody>\n</table>\n<p>362450 rows × 11 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 4
    }
   ],
   "source": [
    "tactic_state = pd.read_json(\n",
    "    DATA_DIRECTORY / \"raw_traced_data\" / \"tactic_state.jsonl\",\n",
    "    orient=\"records\",\n",
    "    lines=True \n",
    ")\n",
    "tactic_state"
   ]
  },
  {
   "source": [
    "`tactic_state_goal.json` includes basic tactic state goal information both before and after the tactic executes."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                    table                   key        tactic_state  \\\n",
       "0       tactic_state_goal  2001:20:2:1:before:0  2001:20:2:1:before   \n",
       "1       tactic_state_goal   2001:20:2:1:after:0   2001:20:2:1:after   \n",
       "2       tactic_state_goal   2016:4:1:1:before:0   2016:4:1:1:before   \n",
       "3       tactic_state_goal    2016:4:1:1:after:0    2016:4:1:1:after   \n",
       "4       tactic_state_goal   2010:4:1:1:before:0   2010:4:1:1:before   \n",
       "...                   ...                   ...                 ...   \n",
       "362445  tactic_state_goal     74:30:2:1:after:0     74:30:2:1:after   \n",
       "362446  tactic_state_goal    74:60:1:1:before:0    74:60:1:1:before   \n",
       "362447  tactic_state_goal     74:60:1:1:after:0     74:60:1:1:after   \n",
       "362448  tactic_state_goal    83:18:1:1:before:0    83:18:1:1:before   \n",
       "362449  tactic_state_goal     83:18:1:1:after:0     83:18:1:1:after   \n",
       "\n",
       "                                                 filename  trace_pos_line  \\\n",
       "0                 lean/library/init/meta/interactive.lean            2033   \n",
       "1                 lean/library/init/meta/interactive.lean            2033   \n",
       "2                 lean/library/init/meta/interactive.lean            2016   \n",
       "3                 lean/library/init/meta/interactive.lean            2016   \n",
       "4                 lean/library/init/meta/interactive.lean            2010   \n",
       "...                                                   ...             ...   \n",
       "362445  mathlib/src/category_theory/abelian/projective...              74   \n",
       "362446  mathlib/src/category_theory/abelian/projective...              74   \n",
       "362447  mathlib/src/category_theory/abelian/projective...              74   \n",
       "362448  mathlib/src/category_theory/abelian/projective...              83   \n",
       "362449  mathlib/src/category_theory/abelian/projective...              83   \n",
       "\n",
       "        trace_pos_column  ix   goal_hash  \\\n",
       "0                      1   0  1078517132   \n",
       "1                      1   0  1080190384   \n",
       "2                      4   0  1786353986   \n",
       "3                      4   0           0   \n",
       "4                      4   0   508157654   \n",
       "...                  ...  ..         ...   \n",
       "362445                30   0           0   \n",
       "362446                60   0  1843829988   \n",
       "362447                60   0           0   \n",
       "362448                18   0  1135957380   \n",
       "362449                18   0           0   \n",
       "\n",
       "                                                  goal_pp  \n",
       "0       α : Type u,\\nh₁ : α,\\nt₁ : list α,\\nh₂ : α,\\nt...  \n",
       "1       α : Type u,\\nh₁ : α,\\nt₁ : list α,\\nh₂ : α,\\nt...  \n",
       "2       α : Sort u,\\nβ : Sort v,\\na₁ a₂ : α\\n⊢ psum.in...  \n",
       "3                                                          \n",
       "4       α : Type u,\\nβ : Type v,\\na₁ a₂ : α\\n⊢ sum.inl...  \n",
       "...                                                   ...  \n",
       "362445                                                     \n",
       "362446  C : Type u,\\n_inst_1 : category_theory.categor...  \n",
       "362447                                                     \n",
       "362448  C : Type u,\\n_inst_1 : category_theory.categor...  \n",
       "362449                                                     \n",
       "\n",
       "[362450 rows x 9 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>table</th>\n      <th>key</th>\n      <th>tactic_state</th>\n      <th>filename</th>\n      <th>trace_pos_line</th>\n      <th>trace_pos_column</th>\n      <th>ix</th>\n      <th>goal_hash</th>\n      <th>goal_pp</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>tactic_state_goal</td>\n      <td>2001:20:2:1:before:0</td>\n      <td>2001:20:2:1:before</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2033</td>\n      <td>1</td>\n      <td>0</td>\n      <td>1078517132</td>\n      <td>α : Type u,\\nh₁ : α,\\nt₁ : list α,\\nh₂ : α,\\nt...</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>tactic_state_goal</td>\n      <td>2001:20:2:1:after:0</td>\n      <td>2001:20:2:1:after</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2033</td>\n      <td>1</td>\n      <td>0</td>\n      <td>1080190384</td>\n      <td>α : Type u,\\nh₁ : α,\\nt₁ : list α,\\nh₂ : α,\\nt...</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>tactic_state_goal</td>\n      <td>2016:4:1:1:before:0</td>\n      <td>2016:4:1:1:before</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2016</td>\n      <td>4</td>\n      <td>0</td>\n      <td>1786353986</td>\n      <td>α : Sort u,\\nβ : Sort v,\\na₁ a₂ : α\\n⊢ psum.in...</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>tactic_state_goal</td>\n      <td>2016:4:1:1:after:0</td>\n      <td>2016:4:1:1:after</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2016</td>\n      <td>4</td>\n      <td>0</td>\n      <td>0</td>\n      <td></td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>tactic_state_goal</td>\n      <td>2010:4:1:1:before:0</td>\n      <td>2010:4:1:1:before</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>2010</td>\n      <td>4</td>\n      <td>0</td>\n      <td>508157654</td>\n      <td>α : Type u,\\nβ : Type v,\\na₁ a₂ : α\\n⊢ sum.inl...</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>362445</th>\n      <td>tactic_state_goal</td>\n      <td>74:30:2:1:after:0</td>\n      <td>74:30:2:1:after</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>30</td>\n      <td>0</td>\n      <td>0</td>\n      <td></td>\n    </tr>\n    <tr>\n      <th>362446</th>\n      <td>tactic_state_goal</td>\n      <td>74:60:1:1:before:0</td>\n      <td>74:60:1:1:before</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>60</td>\n      <td>0</td>\n      <td>1843829988</td>\n      <td>C : Type u,\\n_inst_1 : category_theory.categor...</td>\n    </tr>\n    <tr>\n      <th>362447</th>\n      <td>tactic_state_goal</td>\n      <td>74:60:1:1:after:0</td>\n      <td>74:60:1:1:after</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>74</td>\n      <td>60</td>\n      <td>0</td>\n      <td>0</td>\n      <td></td>\n    </tr>\n    <tr>\n      <th>362448</th>\n      <td>tactic_state_goal</td>\n      <td>83:18:1:1:before:0</td>\n      <td>83:18:1:1:before</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>83</td>\n      <td>18</td>\n      <td>0</td>\n      <td>1135957380</td>\n      <td>C : Type u,\\n_inst_1 : category_theory.categor...</td>\n    </tr>\n    <tr>\n      <th>362449</th>\n      <td>tactic_state_goal</td>\n      <td>83:18:1:1:after:0</td>\n      <td>83:18:1:1:after</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>83</td>\n      <td>18</td>\n      <td>0</td>\n      <td>0</td>\n      <td></td>\n    </tr>\n  </tbody>\n</table>\n<p>362450 rows × 9 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 5
    }
   ],
   "source": [
    "tactic_state_goal = pd.read_json(\n",
    "    DATA_DIRECTORY / \"raw_traced_data\" / \"tactic_state_goal.jsonl\",\n",
    "    orient='records',\n",
    "    lines=True\n",
    ")\n",
    "tactic_state_goal"
   ]
  },
  {
   "source": [
    "`tactic_param_pos` includes position data for every *interactive* tactic parameter.  There are some parameters which are not included since they don't go through the parser."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                   table      key  line  \\\n",
       "0       tactic_param_pos   1985:9  1985   \n",
       "1       tactic_param_pos   1998:9  1998   \n",
       "2       tactic_param_pos   1999:9  1999   \n",
       "3       tactic_param_pos  2001:11  2001   \n",
       "4       tactic_param_pos  2001:18  2001   \n",
       "...                  ...      ...   ...   \n",
       "210066  tactic_param_pos    72:47    72   \n",
       "210067  tactic_param_pos    73:22    73   \n",
       "210068  tactic_param_pos    74:25    74   \n",
       "210069  tactic_param_pos    74:38    74   \n",
       "210070  tactic_param_pos    74:46    74   \n",
       "\n",
       "                                                 filename  trace_pos_line  \\\n",
       "0                 lean/library/init/meta/interactive.lean            1983   \n",
       "1                 lean/library/init/meta/interactive.lean            1983   \n",
       "2                 lean/library/init/meta/interactive.lean            1983   \n",
       "3                 lean/library/init/meta/interactive.lean            1983   \n",
       "4                 lean/library/init/meta/interactive.lean            1983   \n",
       "...                                                   ...             ...   \n",
       "210066  mathlib/src/category_theory/abelian/projective...              67   \n",
       "210067  mathlib/src/category_theory/abelian/projective...              67   \n",
       "210068  mathlib/src/category_theory/abelian/projective...              67   \n",
       "210069  mathlib/src/category_theory/abelian/projective...              67   \n",
       "210070  mathlib/src/category_theory/abelian/projective...              67   \n",
       "\n",
       "        trace_pos_column  column  end_line  end_column  \n",
       "0                      6       9      1985           9  \n",
       "1                      6       9      1998          23  \n",
       "2                      6       9      1999          25  \n",
       "3                      6      11      2001          12  \n",
       "4                      6      18      2001          43  \n",
       "...                  ...     ...       ...         ...  \n",
       "210066                16      47        72          73  \n",
       "210067                16      22        73          54  \n",
       "210068                16      25        74          30  \n",
       "210069                16      38        74          38  \n",
       "210070                16      46        74          55  \n",
       "\n",
       "[210071 rows x 9 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>table</th>\n      <th>key</th>\n      <th>line</th>\n      <th>filename</th>\n      <th>trace_pos_line</th>\n      <th>trace_pos_column</th>\n      <th>column</th>\n      <th>end_line</th>\n      <th>end_column</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>tactic_param_pos</td>\n      <td>1985:9</td>\n      <td>1985</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n      <td>9</td>\n      <td>1985</td>\n      <td>9</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>tactic_param_pos</td>\n      <td>1998:9</td>\n      <td>1998</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n      <td>9</td>\n      <td>1998</td>\n      <td>23</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>tactic_param_pos</td>\n      <td>1999:9</td>\n      <td>1999</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n      <td>9</td>\n      <td>1999</td>\n      <td>25</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>tactic_param_pos</td>\n      <td>2001:11</td>\n      <td>2001</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n      <td>11</td>\n      <td>2001</td>\n      <td>12</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>tactic_param_pos</td>\n      <td>2001:18</td>\n      <td>2001</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n      <td>18</td>\n      <td>2001</td>\n      <td>43</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>210066</th>\n      <td>tactic_param_pos</td>\n      <td>72:47</td>\n      <td>72</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n      <td>47</td>\n      <td>72</td>\n      <td>73</td>\n    </tr>\n    <tr>\n      <th>210067</th>\n      <td>tactic_param_pos</td>\n      <td>73:22</td>\n      <td>73</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n      <td>22</td>\n      <td>73</td>\n      <td>54</td>\n    </tr>\n    <tr>\n      <th>210068</th>\n      <td>tactic_param_pos</td>\n      <td>74:25</td>\n      <td>74</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n      <td>25</td>\n      <td>74</td>\n      <td>30</td>\n    </tr>\n    <tr>\n      <th>210069</th>\n      <td>tactic_param_pos</td>\n      <td>74:38</td>\n      <td>74</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n      <td>38</td>\n      <td>74</td>\n      <td>38</td>\n    </tr>\n    <tr>\n      <th>210070</th>\n      <td>tactic_param_pos</td>\n      <td>74:46</td>\n      <td>74</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n      <td>46</td>\n      <td>74</td>\n      <td>55</td>\n    </tr>\n  </tbody>\n</table>\n<p>210071 rows × 9 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 6
    }
   ],
   "source": [
    "tactic_param_pos = pd.read_json(\n",
    "    DATA_DIRECTORY / \"raw_traced_data\" / \"tactic_param_pos.jsonl\", \n",
    "    orient='records',\n",
    "    lines=True\n",
    ")\n",
    "tactic_param_pos"
   ]
  },
  {
   "source": [
    "`tactic_param_value` includes a pretty printed version of the value passed to the tactic argument.  This is not necessarily how it appears in the lean code, but it is how Lean internally receives the data.  A user could add more tracing code to present this in more ways."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                     table      key  \\\n",
       "0       tactic_param_value   1985:9   \n",
       "1       tactic_param_value   1998:9   \n",
       "2       tactic_param_value   1999:9   \n",
       "3       tactic_param_value  2001:11   \n",
       "4       tactic_param_value  2001:34   \n",
       "...                    ...      ...   \n",
       "210066  tactic_param_value    72:47   \n",
       "210067  tactic_param_value    73:22   \n",
       "210068  tactic_param_value    74:25   \n",
       "210069  tactic_param_value    74:38   \n",
       "210070  tactic_param_value    74:46   \n",
       "\n",
       "                                        reflected_expr_pp  \\\n",
       "0                                                list.nil   \n",
       "1                                      ``(_root_.propext)   \n",
       "2                                    ``(_root_.iff.intro)   \n",
       "3                some (name.mk_string \"_\" name.anonymous)   \n",
       "4                                                 some ()   \n",
       "...                                                   ...   \n",
       "210066                     ``(projective.projective_over)   \n",
       "210067                some ``(exact_d_f (projective.π Z))   \n",
       "210068  sum.inl\\n  [tactic.rcases_patt.alts\\n      [ta...   \n",
       "210069                          interactive.loc.ns [none]   \n",
       "210070                                      ``(exact_d_f)   \n",
       "\n",
       "                                                 filename  trace_pos_line  \\\n",
       "0                 lean/library/init/meta/interactive.lean            1983   \n",
       "1                 lean/library/init/meta/interactive.lean            1983   \n",
       "2                 lean/library/init/meta/interactive.lean            1983   \n",
       "3                 lean/library/init/meta/interactive.lean            1983   \n",
       "4                 lean/library/init/meta/interactive.lean            1983   \n",
       "...                                                   ...             ...   \n",
       "210066  mathlib/src/category_theory/abelian/projective...              67   \n",
       "210067  mathlib/src/category_theory/abelian/projective...              67   \n",
       "210068  mathlib/src/category_theory/abelian/projective...              67   \n",
       "210069  mathlib/src/category_theory/abelian/projective...              67   \n",
       "210070  mathlib/src/category_theory/abelian/projective...              67   \n",
       "\n",
       "        trace_pos_column  \n",
       "0                      6  \n",
       "1                      6  \n",
       "2                      6  \n",
       "3                      6  \n",
       "4                      6  \n",
       "...                  ...  \n",
       "210066                16  \n",
       "210067                16  \n",
       "210068                16  \n",
       "210069                16  \n",
       "210070                16  \n",
       "\n",
       "[210071 rows x 6 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>table</th>\n      <th>key</th>\n      <th>reflected_expr_pp</th>\n      <th>filename</th>\n      <th>trace_pos_line</th>\n      <th>trace_pos_column</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>tactic_param_value</td>\n      <td>1985:9</td>\n      <td>list.nil</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>tactic_param_value</td>\n      <td>1998:9</td>\n      <td>``(_root_.propext)</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>tactic_param_value</td>\n      <td>1999:9</td>\n      <td>``(_root_.iff.intro)</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>tactic_param_value</td>\n      <td>2001:11</td>\n      <td>some (name.mk_string \"_\" name.anonymous)</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>tactic_param_value</td>\n      <td>2001:34</td>\n      <td>some ()</td>\n      <td>lean/library/init/meta/interactive.lean</td>\n      <td>1983</td>\n      <td>6</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>210066</th>\n      <td>tactic_param_value</td>\n      <td>72:47</td>\n      <td>``(projective.projective_over)</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n    </tr>\n    <tr>\n      <th>210067</th>\n      <td>tactic_param_value</td>\n      <td>73:22</td>\n      <td>some ``(exact_d_f (projective.π Z))</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n    </tr>\n    <tr>\n      <th>210068</th>\n      <td>tactic_param_value</td>\n      <td>74:25</td>\n      <td>sum.inl\\n  [tactic.rcases_patt.alts\\n      [ta...</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n    </tr>\n    <tr>\n      <th>210069</th>\n      <td>tactic_param_value</td>\n      <td>74:38</td>\n      <td>interactive.loc.ns [none]</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n    </tr>\n    <tr>\n      <th>210070</th>\n      <td>tactic_param_value</td>\n      <td>74:46</td>\n      <td>``(exact_d_f)</td>\n      <td>mathlib/src/category_theory/abelian/projective...</td>\n      <td>67</td>\n      <td>16</td>\n    </tr>\n  </tbody>\n</table>\n<p>210071 rows × 6 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 7
    }
   ],
   "source": [
    "tactic_param_value = pd.read_json(\n",
    "    DATA_DIRECTORY / \"raw_traced_data\" / \"tactic_param_value.jsonl\",\n",
    "    orient='records',\n",
    "    lines=True\n",
    ")\n",
    "tactic_param_value"
   ]
  },
  {
   "source": [
    "## Extracted Proof Data"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "`proof_trees.json` is a list of abstract syntax trees for each proof.  It doesn't contain much data itself, but has keys to rows in the following tables.  (Unlike the other datasets, this is not a 2D table.)"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "{'key': 'lean/library/data/buffer.lean:49:1',\n",
       " 'node_type': 'proof',\n",
       " 'node_subtype': 'by',\n",
       " 'tactic': {'key': 'lean/library/data/buffer.lean:49:30',\n",
       "  'node_type': 'tactic',\n",
       "  'node_subtype': 'semicolon',\n",
       "  'tactic1': {'key': 'lean/library/data/buffer.lean:49:11',\n",
       "   'node_type': 'tactic',\n",
       "   'node_subtype': 'semicolon',\n",
       "   'tactic1': {'key': 'lean/library/data/buffer.lean:49:4',\n",
       "    'node_type': 'tactic',\n",
       "    'node_subtype': 'named',\n",
       "    'args': [{'key': 'lean/library/data/buffer.lean:49:10',\n",
       "      'node_type': 'tactic_arg',\n",
       "      'node_subtype': 'expression'},\n",
       "     {'key': 'lean/library/data/buffer.lean:49:11',\n",
       "      'node_type': 'tactic_arg',\n",
       "      'node_subtype': 'expression'}]},\n",
       "   'tactic2': {'key': 'lean/library/data/buffer.lean:49:13',\n",
       "    'node_type': 'tactic',\n",
       "    'node_subtype': 'named',\n",
       "    'args': [{'key': 'lean/library/data/buffer.lean:49:20',\n",
       "      'node_type': 'tactic_arg',\n",
       "      'node_subtype': 'expression'},\n",
       "     {'key': 'lean/library/data/buffer.lean:49:30',\n",
       "      'node_type': 'tactic_arg',\n",
       "      'node_subtype': 'expression'}]}},\n",
       "  'tactic2': {'key': 'lean/library/data/buffer.lean:49:32',\n",
       "   'node_type': 'tactic',\n",
       "   'node_subtype': 'named',\n",
       "   'args': [{'key': 'lean/library/data/buffer.lean:49:37',\n",
       "     'node_type': 'tactic_arg',\n",
       "     'node_subtype': 'expression'},\n",
       "    {'key': 'lean/library/data/buffer.lean:51:1',\n",
       "     'node_type': 'tactic_arg',\n",
       "     'node_subtype': 'expression'}]}}}"
      ]
     },
     "metadata": {},
     "execution_count": 8
    }
   ],
   "source": [
    "with jsonlines.open(DATA_DIRECTORY / \"extracted_proof_data\" / \"proof_trees.jsonl\") as f:\n",
    "    proof_trees = list(f)\n",
    "proof_trees[0]"
   ]
  },
  {
   "source": [
    "`proofs.json` contains the Lean human-written text for all tactic proofs along with some other extracted information."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                                                  key  \\\n",
       "0                  lean/library/data/buffer.lean:49:1   \n",
       "1                  lean/library/data/buffer.lean:53:1   \n",
       "2           lean/library/data/buffer/parser.lean:29:1   \n",
       "3           lean/library/data/buffer/parser.lean:38:1   \n",
       "4                  lean/library/data/dlist.lean:50:26   \n",
       "...                                               ...   \n",
       "41151  mathlib/src/topology/vector_bundle.lean:222:24   \n",
       "41152  mathlib/src/topology/vector_bundle.lean:224:25   \n",
       "41153  mathlib/src/topology/vector_bundle.lean:230:16   \n",
       "41154  mathlib/src/topology/vector_bundle.lean:237:21   \n",
       "41155  mathlib/src/topology/vector_bundle.lean:238:48   \n",
       "\n",
       "                                      filename  start_line  start_column  \\\n",
       "0                lean/library/data/buffer.lean          49             1   \n",
       "1                lean/library/data/buffer.lean          53             1   \n",
       "2         lean/library/data/buffer/parser.lean          29             1   \n",
       "3         lean/library/data/buffer/parser.lean          38             1   \n",
       "4                 lean/library/data/dlist.lean          50            26   \n",
       "...                                        ...         ...           ...   \n",
       "41151  mathlib/src/topology/vector_bundle.lean         222            24   \n",
       "41152  mathlib/src/topology/vector_bundle.lean         224            25   \n",
       "41153  mathlib/src/topology/vector_bundle.lean         230            16   \n",
       "41154  mathlib/src/topology/vector_bundle.lean         237            21   \n",
       "41155  mathlib/src/topology/vector_bundle.lean         238            48   \n",
       "\n",
       "       end_line  end_column  \\\n",
       "0            51           1   \n",
       "1            55           1   \n",
       "2            36           1   \n",
       "3            47           1   \n",
       "4            50          63   \n",
       "...         ...         ...   \n",
       "41151       223          89   \n",
       "41152       226          23   \n",
       "41153       230          45   \n",
       "41154       242           6   \n",
       "41155       238          66   \n",
       "\n",
       "                                             code_string  class parent_key  \\\n",
       "0      by cases b; unfold read read'; simp [array.rea...     by              \n",
       "1      by cases b; unfold write write'; simp [array.w...     by              \n",
       "2      begin apply funext, intro input, apply funext,...  begin              \n",
       "3      begin apply funext, intro input, apply funext,...  begin              \n",
       "4                  by abstract { intros, simp, rw [←h] }     by              \n",
       "...                                                  ...    ...        ...   \n",
       "41151  by { rw [←continuous_iff_continuous_on_univ, c...     by              \n",
       "41152  by { rw [←continuous_iff_continuous_on_univ, c...     by              \n",
       "41153                      by simp only [univ_prod_univ]     by              \n",
       "41154  begin have : (λ (x : trivial B F b), x) = @id ...  begin              \n",
       "41155                                 by { ext x, refl }     by              \n",
       "\n",
       "      parent_type  index  line  column  \\\n",
       "0                      0    49       1   \n",
       "1                      0    53       1   \n",
       "2                      0    29       1   \n",
       "3                      0    38       1   \n",
       "4                      0    50      26   \n",
       "...           ...    ...   ...     ...   \n",
       "41151                  0   222      24   \n",
       "41152                  0   224      25   \n",
       "41153                  0   230      16   \n",
       "41154                  0   237      21   \n",
       "41155                  0   238      48   \n",
       "\n",
       "                                     first_tactic_key  \n",
       "0                 lean/library/data/buffer.lean:49:30  \n",
       "1                 lean/library/data/buffer.lean:53:32  \n",
       "2           lean/library/data/buffer/parser.lean:30:1  \n",
       "3           lean/library/data/buffer/parser.lean:39:1  \n",
       "4                  lean/library/data/dlist.lean:50:29  \n",
       "...                                               ...  \n",
       "41151  mathlib/src/topology/vector_bundle.lean:222:27  \n",
       "41152  mathlib/src/topology/vector_bundle.lean:224:28  \n",
       "41153  mathlib/src/topology/vector_bundle.lean:230:19  \n",
       "41154   mathlib/src/topology/vector_bundle.lean:238:5  \n",
       "41155  mathlib/src/topology/vector_bundle.lean:238:51  \n",
       "\n",
       "[41156 rows x 14 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>key</th>\n      <th>filename</th>\n      <th>start_line</th>\n      <th>start_column</th>\n      <th>end_line</th>\n      <th>end_column</th>\n      <th>code_string</th>\n      <th>class</th>\n      <th>parent_key</th>\n      <th>parent_type</th>\n      <th>index</th>\n      <th>line</th>\n      <th>column</th>\n      <th>first_tactic_key</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>1</td>\n      <td>51</td>\n      <td>1</td>\n      <td>by cases b; unfold read read'; simp [array.rea...</td>\n      <td>by</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>49</td>\n      <td>1</td>\n      <td>lean/library/data/buffer.lean:49:30</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>lean/library/data/buffer.lean:53:1</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>53</td>\n      <td>1</td>\n      <td>55</td>\n      <td>1</td>\n      <td>by cases b; unfold write write'; simp [array.w...</td>\n      <td>by</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>53</td>\n      <td>1</td>\n      <td>lean/library/data/buffer.lean:53:32</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>lean/library/data/buffer/parser.lean:29:1</td>\n      <td>lean/library/data/buffer/parser.lean</td>\n      <td>29</td>\n      <td>1</td>\n      <td>36</td>\n      <td>1</td>\n      <td>begin apply funext, intro input, apply funext,...</td>\n      <td>begin</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>29</td>\n      <td>1</td>\n      <td>lean/library/data/buffer/parser.lean:30:1</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>lean/library/data/buffer/parser.lean:38:1</td>\n      <td>lean/library/data/buffer/parser.lean</td>\n      <td>38</td>\n      <td>1</td>\n      <td>47</td>\n      <td>1</td>\n      <td>begin apply funext, intro input, apply funext,...</td>\n      <td>begin</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>38</td>\n      <td>1</td>\n      <td>lean/library/data/buffer/parser.lean:39:1</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>lean/library/data/dlist.lean:50:26</td>\n      <td>lean/library/data/dlist.lean</td>\n      <td>50</td>\n      <td>26</td>\n      <td>50</td>\n      <td>63</td>\n      <td>by abstract { intros, simp, rw [←h] }</td>\n      <td>by</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>50</td>\n      <td>26</td>\n      <td>lean/library/data/dlist.lean:50:29</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>41151</th>\n      <td>mathlib/src/topology/vector_bundle.lean:222:24</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>222</td>\n      <td>24</td>\n      <td>223</td>\n      <td>89</td>\n      <td>by { rw [←continuous_iff_continuous_on_univ, c...</td>\n      <td>by</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>222</td>\n      <td>24</td>\n      <td>mathlib/src/topology/vector_bundle.lean:222:27</td>\n    </tr>\n    <tr>\n      <th>41152</th>\n      <td>mathlib/src/topology/vector_bundle.lean:224:25</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>224</td>\n      <td>25</td>\n      <td>226</td>\n      <td>23</td>\n      <td>by { rw [←continuous_iff_continuous_on_univ, c...</td>\n      <td>by</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>224</td>\n      <td>25</td>\n      <td>mathlib/src/topology/vector_bundle.lean:224:28</td>\n    </tr>\n    <tr>\n      <th>41153</th>\n      <td>mathlib/src/topology/vector_bundle.lean:230:16</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>230</td>\n      <td>16</td>\n      <td>230</td>\n      <td>45</td>\n      <td>by simp only [univ_prod_univ]</td>\n      <td>by</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>230</td>\n      <td>16</td>\n      <td>mathlib/src/topology/vector_bundle.lean:230:19</td>\n    </tr>\n    <tr>\n      <th>41154</th>\n      <td>mathlib/src/topology/vector_bundle.lean:237:21</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>237</td>\n      <td>21</td>\n      <td>242</td>\n      <td>6</td>\n      <td>begin have : (λ (x : trivial B F b), x) = @id ...</td>\n      <td>begin</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>237</td>\n      <td>21</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:5</td>\n    </tr>\n    <tr>\n      <th>41155</th>\n      <td>mathlib/src/topology/vector_bundle.lean:238:48</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>48</td>\n      <td>238</td>\n      <td>66</td>\n      <td>by { ext x, refl }</td>\n      <td>by</td>\n      <td></td>\n      <td></td>\n      <td>0</td>\n      <td>238</td>\n      <td>48</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:51</td>\n    </tr>\n  </tbody>\n</table>\n<p>41156 rows × 14 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 9
    }
   ],
   "source": [
    "proofs = pd.read_json(\n",
    "    DATA_DIRECTORY / \"extracted_proof_data\" / \"proofs.jsonl\",\n",
    "    orient=\"records\",\n",
    "    lines=True\n",
    ")\n",
    "proofs"
   ]
  },
  {
   "source": [
    "`tactics.json` contains the Lean human-written text for all tactic commands along with some other extracted information."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                                                   key  \\\n",
       "0                   lean/library/data/buffer.lean:49:4   \n",
       "1                  lean/library/data/buffer.lean:49:13   \n",
       "2                  lean/library/data/buffer.lean:49:11   \n",
       "3                  lean/library/data/buffer.lean:49:32   \n",
       "4                  lean/library/data/buffer.lean:49:30   \n",
       "...                                                ...   \n",
       "175186  mathlib/src/topology/vector_bundle.lean:238:48   \n",
       "175187   mathlib/src/topology/vector_bundle.lean:239:5   \n",
       "175188  mathlib/src/topology/vector_bundle.lean:238:53   \n",
       "175189  mathlib/src/topology/vector_bundle.lean:238:60   \n",
       "175190  mathlib/src/topology/vector_bundle.lean:238:51   \n",
       "\n",
       "                                       filename  start_line  start_column  \\\n",
       "0                 lean/library/data/buffer.lean          49             4   \n",
       "1                 lean/library/data/buffer.lean          49            13   \n",
       "2                 lean/library/data/buffer.lean          49             4   \n",
       "3                 lean/library/data/buffer.lean          49            32   \n",
       "4                 lean/library/data/buffer.lean          49             4   \n",
       "...                                         ...         ...           ...   \n",
       "175186  mathlib/src/topology/vector_bundle.lean         238            48   \n",
       "175187  mathlib/src/topology/vector_bundle.lean         239             5   \n",
       "175188  mathlib/src/topology/vector_bundle.lean         238            53   \n",
       "175189  mathlib/src/topology/vector_bundle.lean         238            60   \n",
       "175190  mathlib/src/topology/vector_bundle.lean         238            51   \n",
       "\n",
       "        end_line  end_column  \\\n",
       "0             49          11   \n",
       "1             49          30   \n",
       "2             49          30   \n",
       "3             51           1   \n",
       "4             51           1   \n",
       "...          ...         ...   \n",
       "175186       238          66   \n",
       "175187       241          18   \n",
       "175188       238          58   \n",
       "175189       238          65   \n",
       "175190       238          66   \n",
       "\n",
       "                                              code_string      class  \\\n",
       "0                                                 cases b      named   \n",
       "1                                       unfold read read'      named   \n",
       "2                              cases b; unfold read read'  semicolon   \n",
       "3                              simp [array.read_eq_read']      named   \n",
       "4       cases b; unfold read read'; simp [array.read_e...  semicolon   \n",
       "...                                                   ...        ...   \n",
       "175186                                 by { ext x, refl }     solve1   \n",
       "175187  simp only [total_space.topological_space, indu...      named   \n",
       "175188                                              ext x      named   \n",
       "175189                                               refl      named   \n",
       "175190                                    { ext x, refl }     solve1   \n",
       "\n",
       "                                            parent_key parent_type  index  \\\n",
       "0                  lean/library/data/buffer.lean:49:11      tactic      0   \n",
       "1                  lean/library/data/buffer.lean:49:11      tactic      1   \n",
       "2                  lean/library/data/buffer.lean:49:30      tactic      0   \n",
       "3                  lean/library/data/buffer.lean:49:30      tactic      1   \n",
       "4                   lean/library/data/buffer.lean:49:1       proof      0   \n",
       "...                                                ...         ...    ...   \n",
       "175186  mathlib/src/topology/vector_bundle.lean:237:21       proof      1   \n",
       "175187  mathlib/src/topology/vector_bundle.lean:237:21       proof      2   \n",
       "175188  mathlib/src/topology/vector_bundle.lean:238:51      tactic      0   \n",
       "175189  mathlib/src/topology/vector_bundle.lean:238:51      tactic      1   \n",
       "175190  mathlib/src/topology/vector_bundle.lean:238:48       proof      0   \n",
       "\n",
       "        line  column                                       proof_key trace_key  \n",
       "0         49       4              lean/library/data/buffer.lean:49:1    49:4:3  \n",
       "1         49      13              lean/library/data/buffer.lean:49:1   49:13:3  \n",
       "2         49      11              lean/library/data/buffer.lean:49:1   49:11:2  \n",
       "3         49      32              lean/library/data/buffer.lean:49:1   49:32:2  \n",
       "4         49      30              lean/library/data/buffer.lean:49:1   49:11:1  \n",
       "...      ...     ...                                             ...       ...  \n",
       "175186   238      48  mathlib/src/topology/vector_bundle.lean:237:21            \n",
       "175187   239       5  mathlib/src/topology/vector_bundle.lean:237:21   239:5:1  \n",
       "175188   238      53  mathlib/src/topology/vector_bundle.lean:238:48  238:53:3  \n",
       "175189   238      60  mathlib/src/topology/vector_bundle.lean:238:48  238:60:3  \n",
       "175190   238      51  mathlib/src/topology/vector_bundle.lean:238:48  238:65:2  \n",
       "\n",
       "[175191 rows x 15 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>key</th>\n      <th>filename</th>\n      <th>start_line</th>\n      <th>start_column</th>\n      <th>end_line</th>\n      <th>end_column</th>\n      <th>code_string</th>\n      <th>class</th>\n      <th>parent_key</th>\n      <th>parent_type</th>\n      <th>index</th>\n      <th>line</th>\n      <th>column</th>\n      <th>proof_key</th>\n      <th>trace_key</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>lean/library/data/buffer.lean:49:4</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>4</td>\n      <td>49</td>\n      <td>11</td>\n      <td>cases b</td>\n      <td>named</td>\n      <td>lean/library/data/buffer.lean:49:11</td>\n      <td>tactic</td>\n      <td>0</td>\n      <td>49</td>\n      <td>4</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>49:4:3</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>lean/library/data/buffer.lean:49:13</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>13</td>\n      <td>49</td>\n      <td>30</td>\n      <td>unfold read read'</td>\n      <td>named</td>\n      <td>lean/library/data/buffer.lean:49:11</td>\n      <td>tactic</td>\n      <td>1</td>\n      <td>49</td>\n      <td>13</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>49:13:3</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>lean/library/data/buffer.lean:49:11</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>4</td>\n      <td>49</td>\n      <td>30</td>\n      <td>cases b; unfold read read'</td>\n      <td>semicolon</td>\n      <td>lean/library/data/buffer.lean:49:30</td>\n      <td>tactic</td>\n      <td>0</td>\n      <td>49</td>\n      <td>11</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>49:11:2</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>lean/library/data/buffer.lean:49:32</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>32</td>\n      <td>51</td>\n      <td>1</td>\n      <td>simp [array.read_eq_read']</td>\n      <td>named</td>\n      <td>lean/library/data/buffer.lean:49:30</td>\n      <td>tactic</td>\n      <td>1</td>\n      <td>49</td>\n      <td>32</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>49:32:2</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>lean/library/data/buffer.lean:49:30</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>4</td>\n      <td>51</td>\n      <td>1</td>\n      <td>cases b; unfold read read'; simp [array.read_e...</td>\n      <td>semicolon</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>proof</td>\n      <td>0</td>\n      <td>49</td>\n      <td>30</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>49:11:1</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>175186</th>\n      <td>mathlib/src/topology/vector_bundle.lean:238:48</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>48</td>\n      <td>238</td>\n      <td>66</td>\n      <td>by { ext x, refl }</td>\n      <td>solve1</td>\n      <td>mathlib/src/topology/vector_bundle.lean:237:21</td>\n      <td>proof</td>\n      <td>1</td>\n      <td>238</td>\n      <td>48</td>\n      <td>mathlib/src/topology/vector_bundle.lean:237:21</td>\n      <td></td>\n    </tr>\n    <tr>\n      <th>175187</th>\n      <td>mathlib/src/topology/vector_bundle.lean:239:5</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>239</td>\n      <td>5</td>\n      <td>241</td>\n      <td>18</td>\n      <td>simp only [total_space.topological_space, indu...</td>\n      <td>named</td>\n      <td>mathlib/src/topology/vector_bundle.lean:237:21</td>\n      <td>proof</td>\n      <td>2</td>\n      <td>239</td>\n      <td>5</td>\n      <td>mathlib/src/topology/vector_bundle.lean:237:21</td>\n      <td>239:5:1</td>\n    </tr>\n    <tr>\n      <th>175188</th>\n      <td>mathlib/src/topology/vector_bundle.lean:238:53</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>53</td>\n      <td>238</td>\n      <td>58</td>\n      <td>ext x</td>\n      <td>named</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:51</td>\n      <td>tactic</td>\n      <td>0</td>\n      <td>238</td>\n      <td>53</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:48</td>\n      <td>238:53:3</td>\n    </tr>\n    <tr>\n      <th>175189</th>\n      <td>mathlib/src/topology/vector_bundle.lean:238:60</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>60</td>\n      <td>238</td>\n      <td>65</td>\n      <td>refl</td>\n      <td>named</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:51</td>\n      <td>tactic</td>\n      <td>1</td>\n      <td>238</td>\n      <td>60</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:48</td>\n      <td>238:60:3</td>\n    </tr>\n    <tr>\n      <th>175190</th>\n      <td>mathlib/src/topology/vector_bundle.lean:238:51</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>51</td>\n      <td>238</td>\n      <td>66</td>\n      <td>{ ext x, refl }</td>\n      <td>solve1</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:48</td>\n      <td>proof</td>\n      <td>0</td>\n      <td>238</td>\n      <td>51</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:48</td>\n      <td>238:65:2</td>\n    </tr>\n  </tbody>\n</table>\n<p>175191 rows × 15 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 10
    }
   ],
   "source": [
    "tactics = pd.read_json(\n",
    "    DATA_DIRECTORY / \"extracted_proof_data\" / \"tactics.jsonl\", \n",
    "    orient='records',\n",
    "    lines=True\n",
    ")\n",
    "tactics"
   ]
  },
  {
   "source": [
    "`args.json` contains the Lean human-written text for all tactic arguements along with some other extracted information."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                                                   key  \\\n",
       "0                  lean/library/data/buffer.lean:49:10   \n",
       "1                  lean/library/data/buffer.lean:49:11   \n",
       "2                  lean/library/data/buffer.lean:49:20   \n",
       "3                  lean/library/data/buffer.lean:49:30   \n",
       "4                  lean/library/data/buffer.lean:49:37   \n",
       "...                                                ...   \n",
       "211820  mathlib/src/topology/vector_bundle.lean:239:10   \n",
       "211821  mathlib/src/topology/vector_bundle.lean:239:15   \n",
       "211822  mathlib/src/topology/vector_bundle.lean:241:18   \n",
       "211823  mathlib/src/topology/vector_bundle.lean:238:57   \n",
       "211824  mathlib/src/topology/vector_bundle.lean:238:58   \n",
       "\n",
       "                                       filename  start_line  start_column  \\\n",
       "0                 lean/library/data/buffer.lean          49            10   \n",
       "1                 lean/library/data/buffer.lean          49            11   \n",
       "2                 lean/library/data/buffer.lean          49            20   \n",
       "3                 lean/library/data/buffer.lean          49            30   \n",
       "4                 lean/library/data/buffer.lean          49            37   \n",
       "...                                         ...         ...           ...   \n",
       "211820  mathlib/src/topology/vector_bundle.lean         239            10   \n",
       "211821  mathlib/src/topology/vector_bundle.lean         239            15   \n",
       "211822  mathlib/src/topology/vector_bundle.lean         241            18   \n",
       "211823  mathlib/src/topology/vector_bundle.lean         238            57   \n",
       "211824  mathlib/src/topology/vector_bundle.lean         238            58   \n",
       "\n",
       "        end_line  end_column  \\\n",
       "0             49          11   \n",
       "1             49          11   \n",
       "2             49          30   \n",
       "3             49          30   \n",
       "4             51           1   \n",
       "...          ...         ...   \n",
       "211820       239          15   \n",
       "211821       241          18   \n",
       "211822       241          18   \n",
       "211823       238          58   \n",
       "211824       238          58   \n",
       "\n",
       "                                              code_string       class  \\\n",
       "0                                                       b  expression   \n",
       "1                                                          expression   \n",
       "2                                              read read'  expression   \n",
       "3                                                          expression   \n",
       "4                                   [array.read_eq_read']  expression   \n",
       "...                                                   ...         ...   \n",
       "211820                                               only  expression   \n",
       "211821  [total_space.topological_space, induced_inf, i...  expression   \n",
       "211822                                                     expression   \n",
       "211823                                                  x  expression   \n",
       "211824                                                     expression   \n",
       "\n",
       "                                            parent_key parent_type  index  \\\n",
       "0                   lean/library/data/buffer.lean:49:4      tactic      0   \n",
       "1                   lean/library/data/buffer.lean:49:4      tactic      1   \n",
       "2                  lean/library/data/buffer.lean:49:13      tactic      0   \n",
       "3                  lean/library/data/buffer.lean:49:13      tactic      1   \n",
       "4                  lean/library/data/buffer.lean:49:32      tactic      0   \n",
       "...                                                ...         ...    ...   \n",
       "211820   mathlib/src/topology/vector_bundle.lean:239:5      tactic      0   \n",
       "211821   mathlib/src/topology/vector_bundle.lean:239:5      tactic      1   \n",
       "211822   mathlib/src/topology/vector_bundle.lean:239:5      tactic      2   \n",
       "211823  mathlib/src/topology/vector_bundle.lean:238:53      tactic      0   \n",
       "211824  mathlib/src/topology/vector_bundle.lean:238:53      tactic      1   \n",
       "\n",
       "        line  column  \n",
       "0         49      10  \n",
       "1         49      11  \n",
       "2         49      20  \n",
       "3         49      30  \n",
       "4         49      37  \n",
       "...      ...     ...  \n",
       "211820   239      10  \n",
       "211821   239      15  \n",
       "211822   241      18  \n",
       "211823   238      57  \n",
       "211824   238      58  \n",
       "\n",
       "[211825 rows x 13 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>key</th>\n      <th>filename</th>\n      <th>start_line</th>\n      <th>start_column</th>\n      <th>end_line</th>\n      <th>end_column</th>\n      <th>code_string</th>\n      <th>class</th>\n      <th>parent_key</th>\n      <th>parent_type</th>\n      <th>index</th>\n      <th>line</th>\n      <th>column</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>lean/library/data/buffer.lean:49:10</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>10</td>\n      <td>49</td>\n      <td>11</td>\n      <td>b</td>\n      <td>expression</td>\n      <td>lean/library/data/buffer.lean:49:4</td>\n      <td>tactic</td>\n      <td>0</td>\n      <td>49</td>\n      <td>10</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>lean/library/data/buffer.lean:49:11</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>11</td>\n      <td>49</td>\n      <td>11</td>\n      <td></td>\n      <td>expression</td>\n      <td>lean/library/data/buffer.lean:49:4</td>\n      <td>tactic</td>\n      <td>1</td>\n      <td>49</td>\n      <td>11</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>lean/library/data/buffer.lean:49:20</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>20</td>\n      <td>49</td>\n      <td>30</td>\n      <td>read read'</td>\n      <td>expression</td>\n      <td>lean/library/data/buffer.lean:49:13</td>\n      <td>tactic</td>\n      <td>0</td>\n      <td>49</td>\n      <td>20</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>lean/library/data/buffer.lean:49:30</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>30</td>\n      <td>49</td>\n      <td>30</td>\n      <td></td>\n      <td>expression</td>\n      <td>lean/library/data/buffer.lean:49:13</td>\n      <td>tactic</td>\n      <td>1</td>\n      <td>49</td>\n      <td>30</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>lean/library/data/buffer.lean:49:37</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>37</td>\n      <td>51</td>\n      <td>1</td>\n      <td>[array.read_eq_read']</td>\n      <td>expression</td>\n      <td>lean/library/data/buffer.lean:49:32</td>\n      <td>tactic</td>\n      <td>0</td>\n      <td>49</td>\n      <td>37</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>211820</th>\n      <td>mathlib/src/topology/vector_bundle.lean:239:10</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>239</td>\n      <td>10</td>\n      <td>239</td>\n      <td>15</td>\n      <td>only</td>\n      <td>expression</td>\n      <td>mathlib/src/topology/vector_bundle.lean:239:5</td>\n      <td>tactic</td>\n      <td>0</td>\n      <td>239</td>\n      <td>10</td>\n    </tr>\n    <tr>\n      <th>211821</th>\n      <td>mathlib/src/topology/vector_bundle.lean:239:15</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>239</td>\n      <td>15</td>\n      <td>241</td>\n      <td>18</td>\n      <td>[total_space.topological_space, induced_inf, i...</td>\n      <td>expression</td>\n      <td>mathlib/src/topology/vector_bundle.lean:239:5</td>\n      <td>tactic</td>\n      <td>1</td>\n      <td>239</td>\n      <td>15</td>\n    </tr>\n    <tr>\n      <th>211822</th>\n      <td>mathlib/src/topology/vector_bundle.lean:241:18</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>241</td>\n      <td>18</td>\n      <td>241</td>\n      <td>18</td>\n      <td></td>\n      <td>expression</td>\n      <td>mathlib/src/topology/vector_bundle.lean:239:5</td>\n      <td>tactic</td>\n      <td>2</td>\n      <td>241</td>\n      <td>18</td>\n    </tr>\n    <tr>\n      <th>211823</th>\n      <td>mathlib/src/topology/vector_bundle.lean:238:57</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>57</td>\n      <td>238</td>\n      <td>58</td>\n      <td>x</td>\n      <td>expression</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:53</td>\n      <td>tactic</td>\n      <td>0</td>\n      <td>238</td>\n      <td>57</td>\n    </tr>\n    <tr>\n      <th>211824</th>\n      <td>mathlib/src/topology/vector_bundle.lean:238:58</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>58</td>\n      <td>238</td>\n      <td>58</td>\n      <td></td>\n      <td>expression</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:53</td>\n      <td>tactic</td>\n      <td>1</td>\n      <td>238</td>\n      <td>58</td>\n    </tr>\n  </tbody>\n</table>\n<p>211825 rows × 13 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 11
    }
   ],
   "source": [
    "args = pd.read_json(\n",
    "    DATA_DIRECTORY / \"extracted_proof_data\" / \"args.jsonl\", \n",
    "    orient=\"records\",\n",
    "    lines=True\n",
    ")\n",
    "args"
   ]
  },
  {
   "source": [
    "## Examples of combining data"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "Here we combine the above data sources to make a table containing:\n",
    "* First goals in the goal stack before the tactic is executed\n",
    "* The human written tactic command\n",
    "* A little metadata about the type of tactic.  If a \"named\" tactic, then the tactic name is the first word in the tactic command."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                                                  goal_pp  \\\n",
       "0       α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "1       α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "2       α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...   \n",
       "3       α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...   \n",
       "4       α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "...                                                   ...   \n",
       "183363  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "183364  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "183365  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "183366  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "183367  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "\n",
       "                                        human_tactic_code tactic_class  \n",
       "0       cases b; unfold read read'; simp [array.read_e...    semicolon  \n",
       "1                              cases b; unfold read read'    semicolon  \n",
       "2                                       unfold read read'        named  \n",
       "3                              simp [array.read_eq_read']        named  \n",
       "4                                                 cases b        named  \n",
       "...                                                   ...          ...  \n",
       "183363                                               refl        named  \n",
       "183364                                               refl        named  \n",
       "183365                                    { ext x, refl }       solve1  \n",
       "183366                                    { ext x, refl }       solve1  \n",
       "183367  simp only [total_space.topological_space, indu...        named  \n",
       "\n",
       "[181887 rows x 3 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>goal_pp</th>\n      <th>human_tactic_code</th>\n      <th>tactic_class</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n      <td>cases b; unfold read read'; simp [array.read_e...</td>\n      <td>semicolon</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n      <td>cases b; unfold read read'</td>\n      <td>semicolon</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...</td>\n      <td>unfold read read'</td>\n      <td>named</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...</td>\n      <td>simp [array.read_eq_read']</td>\n      <td>named</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n      <td>cases b</td>\n      <td>named</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>183363</th>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>refl</td>\n      <td>named</td>\n    </tr>\n    <tr>\n      <th>183364</th>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>refl</td>\n      <td>named</td>\n    </tr>\n    <tr>\n      <th>183365</th>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>{ ext x, refl }</td>\n      <td>solve1</td>\n    </tr>\n    <tr>\n      <th>183366</th>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>{ ext x, refl }</td>\n      <td>solve1</td>\n    </tr>\n    <tr>\n      <th>183367</th>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>simp only [total_space.topological_space, indu...</td>\n      <td>named</td>\n    </tr>\n  </tbody>\n</table>\n<p>181887 rows × 3 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 12
    }
   ],
   "source": [
    "df = tactic_state_goal.copy()\n",
    "df = df[df['ix'] == 0]\n",
    "#df['key'] = df['filename'] + \":\" + df['key']\n",
    "df['tactic_state_key'] = df['filename'] + \":\" + df['tactic_state']\n",
    "df = df[['tactic_state_key', 'goal_pp']]\n",
    "df = df.set_index('tactic_state_key')\n",
    "\n",
    "df2 = tactic_state.copy()\n",
    "df2 = df2[df2['before_after'] == 'before']\n",
    "df2['tactic_state_key'] = df2['filename'] + \":\" + df2['key']\n",
    "df2['tactic_instance_key'] = df2['filename'] + \":\" + df2['tactic_instance']\n",
    "df2['tactic_key'] = df2['tactic_instance_key'].apply(lambda k: \":\".join(k.split(\":\")[:-1]))\n",
    "df2 = df2[['tactic_state_key', 'tactic_instance_key', 'tactic_key']]\n",
    "df2 = df2.set_index('tactic_state_key')\n",
    "\n",
    "df = df.join(df2)\n",
    "df = df.set_index('tactic_key')\n",
    "df.head()\n",
    "\n",
    "df3 = tactics.copy()\n",
    "df3['tactic_key'] = df3['filename'] + \":\" + df3['trace_key']\n",
    "df3 = df3[['tactic_key', 'code_string', 'class']]\n",
    "df3 = df3.set_index('tactic_key')\n",
    "df = df.join(df3)\n",
    "df = df.reset_index()\n",
    "df = df[['goal_pp', 'code_string', 'class']]\n",
    "df = df.rename(columns={'class': 'tactic_class', 'code_string': 'human_tactic_code'})\n",
    "# some tactics are recorded by the tracing code, but correspond to tactics \n",
    "# instances in a `[...] block in, possibly, another file.  They are dropped here.\n",
    "df = df.dropna()  \n",
    "\n",
    "goals_and_tactics = df\n",
    "goals_and_tactics"
   ]
  },
  {
   "source": [
    "Each named tactic command can have a number of arguments.  Here we seperate the arguments showing both human supplied argument and the internal representation used by Lean."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "output_type": "stream",
     "name": "stderr",
     "text": [
      "/Users/jasonrute/Development/lean/lean_proof_recording/venv/lib/python3.8/site-packages/pandas/core/reshape/merge.py:643: UserWarning: merging between different levels can give an unintended result (1 levels on the left,2 on the right)\n  warnings.warn(msg, UserWarning)\n"
     ]
    },
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "                                                           human_tactic_arg  \\\n",
       "                                                                          0   \n",
       "human_tactic_code                                                             \n",
       "unfold read read'                                                read read'   \n",
       "simp [array.read_eq_read']                            [array.read_eq_read']   \n",
       "cases b                                                                   b   \n",
       "unfold write write'                                            write write'   \n",
       "simp [array.write_eq_write']                        [array.write_eq_write']   \n",
       "...                                                                     ...   \n",
       "ext x                                                                     x   \n",
       "ext x                                                                     x   \n",
       "refl                                                                    NaN   \n",
       "refl                                                                    NaN   \n",
       "simp only [total_space.topological_space, induc...                     only   \n",
       "\n",
       "                                                                                                       \\\n",
       "                                                                                                    1   \n",
       "human_tactic_code                                                                                       \n",
       "unfold read read'                                                                                       \n",
       "simp [array.read_eq_read']                                                                              \n",
       "cases b                                                                                                 \n",
       "unfold write write'                                                                                     \n",
       "simp [array.write_eq_write']                                                                            \n",
       "...                                                                                               ...   \n",
       "ext x                                                                                                   \n",
       "ext x                                                                                                   \n",
       "refl                                                                                              NaN   \n",
       "refl                                                                                              NaN   \n",
       "simp only [total_space.topological_space, induc...  [total_space.topological_space, induced_inf, i...   \n",
       "\n",
       "                                                                   \\\n",
       "                                                      2    3    4   \n",
       "human_tactic_code                                                   \n",
       "unfold read read'                                   NaN  NaN  NaN   \n",
       "simp [array.read_eq_read']                          NaN  NaN  NaN   \n",
       "cases b                                             NaN  NaN  NaN   \n",
       "unfold write write'                                 NaN  NaN  NaN   \n",
       "simp [array.write_eq_write']                        NaN  NaN  NaN   \n",
       "...                                                 ...  ...  ...   \n",
       "ext x                                               NaN  NaN  NaN   \n",
       "ext x                                               NaN  NaN  NaN   \n",
       "refl                                                NaN  NaN  NaN   \n",
       "refl                                                NaN  NaN  NaN   \n",
       "simp only [total_space.topological_space, induc...       NaN  NaN   \n",
       "\n",
       "                                                                                    reflected_expr_pp  \\\n",
       "                                                                                                    0   \n",
       "human_tactic_code                                                                                       \n",
       "unfold read read'                                   [name.mk_string \"read\" name.anonymous, name.mk...   \n",
       "simp [array.read_eq_read']                          [tactic.simp_arg_type.expr ``(array.read_eq_re...   \n",
       "cases b                                                                            (none name, ``(b))   \n",
       "unfold write write'                                 [name.mk_string \"write\" name.anonymous, name.m...   \n",
       "simp [array.write_eq_write']                        [tactic.simp_arg_type.expr ``(array.write_eq_w...   \n",
       "...                                                                                               ...   \n",
       "ext x                                               [tactic.rcases_patt.one (name.mk_string \"x\" na...   \n",
       "ext x                                               [tactic.rcases_patt.one (name.mk_string \"x\" na...   \n",
       "refl                                                                                              NaN   \n",
       "refl                                                                                              NaN   \n",
       "simp only [total_space.topological_space, induc...                                                 tt   \n",
       "\n",
       "                                                                                                       \\\n",
       "                                                                                                    1   \n",
       "human_tactic_code                                                                                       \n",
       "unfold read read'                                                           interactive.loc.ns [none]   \n",
       "simp [array.read_eq_read']                                                  interactive.loc.ns [none]   \n",
       "cases b                                                                                      list.nil   \n",
       "unfold write write'                                                         interactive.loc.ns [none]   \n",
       "simp [array.write_eq_write']                                                interactive.loc.ns [none]   \n",
       "...                                                                                               ...   \n",
       "ext x                                                                                            none   \n",
       "ext x                                                                                            none   \n",
       "refl                                                                                              NaN   \n",
       "refl                                                                                              NaN   \n",
       "simp only [total_space.topological_space, induc...  [tactic.simp_arg_type.expr ``(total_space.topo...   \n",
       "\n",
       "                                                                               \\\n",
       "                                                                            2   \n",
       "human_tactic_code                                                               \n",
       "unfold read read'                                                         NaN   \n",
       "simp [array.read_eq_read']                                                NaN   \n",
       "cases b                                                                   NaN   \n",
       "unfold write write'                                                       NaN   \n",
       "simp [array.write_eq_write']                                              NaN   \n",
       "...                                                                       ...   \n",
       "ext x                                                                     NaN   \n",
       "ext x                                                                     NaN   \n",
       "refl                                                                      NaN   \n",
       "refl                                                                      NaN   \n",
       "simp only [total_space.topological_space, induc...  interactive.loc.ns [none]   \n",
       "\n",
       "                                                              \n",
       "                                                      3    4  \n",
       "human_tactic_code                                             \n",
       "unfold read read'                                   NaN  NaN  \n",
       "simp [array.read_eq_read']                          NaN  NaN  \n",
       "cases b                                             NaN  NaN  \n",
       "unfold write write'                                 NaN  NaN  \n",
       "simp [array.write_eq_write']                        NaN  NaN  \n",
       "...                                                 ...  ...  \n",
       "ext x                                               NaN  NaN  \n",
       "ext x                                               NaN  NaN  \n",
       "refl                                                NaN  NaN  \n",
       "refl                                                NaN  NaN  \n",
       "simp only [total_space.topological_space, induc...  NaN  NaN  \n",
       "\n",
       "[138256 rows x 10 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead tr th {\n        text-align: left;\n    }\n\n    .dataframe thead tr:last-of-type th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr>\n      <th></th>\n      <th colspan=\"5\" halign=\"left\">human_tactic_arg</th>\n      <th colspan=\"5\" halign=\"left\">reflected_expr_pp</th>\n    </tr>\n    <tr>\n      <th></th>\n      <th>0</th>\n      <th>1</th>\n      <th>2</th>\n      <th>3</th>\n      <th>4</th>\n      <th>0</th>\n      <th>1</th>\n      <th>2</th>\n      <th>3</th>\n      <th>4</th>\n    </tr>\n    <tr>\n      <th>human_tactic_code</th>\n      <th></th>\n      <th></th>\n      <th></th>\n      <th></th>\n      <th></th>\n      <th></th>\n      <th></th>\n      <th></th>\n      <th></th>\n      <th></th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>unfold read read'</th>\n      <td>read read'</td>\n      <td></td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>[name.mk_string \"read\" name.anonymous, name.mk...</td>\n      <td>interactive.loc.ns [none]</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>simp [array.read_eq_read']</th>\n      <td>[array.read_eq_read']</td>\n      <td></td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>[tactic.simp_arg_type.expr ``(array.read_eq_re...</td>\n      <td>interactive.loc.ns [none]</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>cases b</th>\n      <td>b</td>\n      <td></td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>(none name, ``(b))</td>\n      <td>list.nil</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>unfold write write'</th>\n      <td>write write'</td>\n      <td></td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>[name.mk_string \"write\" name.anonymous, name.m...</td>\n      <td>interactive.loc.ns [none]</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>simp [array.write_eq_write']</th>\n      <td>[array.write_eq_write']</td>\n      <td></td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>[tactic.simp_arg_type.expr ``(array.write_eq_w...</td>\n      <td>interactive.loc.ns [none]</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>ext x</th>\n      <td>x</td>\n      <td></td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>[tactic.rcases_patt.one (name.mk_string \"x\" na...</td>\n      <td>none</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>ext x</th>\n      <td>x</td>\n      <td></td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>[tactic.rcases_patt.one (name.mk_string \"x\" na...</td>\n      <td>none</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>refl</th>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>refl</th>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n    <tr>\n      <th>simp only [total_space.topological_space, induced_inf, induced_compose, function.comp, proj, induced_const, top_inf_eq, trivial.proj_snd, id.def, trivial.topological_space, this, induced_id]</th>\n      <td>only</td>\n      <td>[total_space.topological_space, induced_inf, i...</td>\n      <td></td>\n      <td>NaN</td>\n      <td>NaN</td>\n      <td>tt</td>\n      <td>[tactic.simp_arg_type.expr ``(total_space.topo...</td>\n      <td>interactive.loc.ns [none]</td>\n      <td>NaN</td>\n      <td>NaN</td>\n    </tr>\n  </tbody>\n</table>\n<p>138256 rows × 10 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 13
    }
   ],
   "source": [
    "# the lean internal values are indexed by the starting position of\n",
    "# the parameter argument.  Unfortionately, because of zero length\n",
    "# arguments, two different arguements can have the same starting\n",
    "# position.  We add an cumulative count to address this.\n",
    "df = tactic_param_value.copy()\n",
    "df['key'] = df['filename'] + \":\" + df['key']\n",
    "df['cnt'] = df.groupby('key').cumcount()\n",
    "df['key2'] = df['key'] + \":\" + df['cnt'].astype(str)\n",
    "df = df.set_index('key2')\n",
    "df = df[['reflected_expr_pp']]\n",
    "\n",
    "df2 = args.copy()\n",
    "# args has duplicates since there is a \n",
    "# line for each tactic execution instance\n",
    "df2 = df2.drop_duplicates()  \n",
    "df2['cnt'] = df2.groupby('key').cumcount()\n",
    "df2['key2'] = df2['key'] + \":\" + df2['cnt'].astype(str)\n",
    "df2 = df2.set_index('key2')\n",
    "df2 = df2.rename(columns={'code_string': 'human_tactic_arg'})\n",
    "df2 = df2[['parent_key', 'index', 'human_tactic_arg']]\n",
    "\n",
    "df3 = df2.join(df).reset_index()[['parent_key', 'index', 'human_tactic_arg', 'reflected_expr_pp']]\n",
    "df3 = df3.set_index('parent_key')\n",
    "df3 = df3.pivot_table(\n",
    "    values=['human_tactic_arg', 'reflected_expr_pp'],\n",
    "    index='parent_key',\n",
    "    columns='index',\n",
    "    aggfunc='first'\n",
    ")\n",
    "\n",
    "df4 = tactics.copy()\n",
    "df4 = df4[df4['class'] == \"named\"]\n",
    "df4 = df4[['key', 'code_string']]\n",
    "df4 = df4.rename(columns={'code_string': 'human_tactic_code'})\n",
    "df4 = df4.set_index('key')\n",
    "\n",
    "parsed_tactics = df4.join(df3)\n",
    "parsed_tactics = parsed_tactics.set_index('human_tactic_code')\n",
    "parsed_tactics.columns = pd.MultiIndex.from_tuples(parsed_tactics.columns)\n",
    "parsed_tactics"
   ]
  },
  {
   "source": [
    "## Training data"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "Below are examples of the extacted and cleaned data used to train Lean GPT-f."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "This is a combined CSV of the training data and metadata.  Note, that the train-valid-test split is deterministic based on a hash of the declaration name.  This makes it simple to combine this data with data from other sources."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "        Unnamed: 0                                            goal_pp  \\\n",
       "0                0  α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "1                1  α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "2                2  α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...   \n",
       "3                3  α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...   \n",
       "4                4  α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...   \n",
       "...            ...                                                ...   \n",
       "181882      181882  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "181883      181883  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "181884      181884  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "181885      181885  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "181886      181886  R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...   \n",
       "\n",
       "                                                decl_name  \\\n",
       "0                                    buffer.read_eq_read'   \n",
       "1                                    buffer.read_eq_read'   \n",
       "2                                    buffer.read_eq_read'   \n",
       "3                                    buffer.read_eq_read'   \n",
       "4                                    buffer.read_eq_read'   \n",
       "...                                                   ...   \n",
       "181882  topological_vector_bundle.trivial_bundle.topol...   \n",
       "181883  topological_vector_bundle.trivial_bundle.topol...   \n",
       "181884  topological_vector_bundle.trivial_bundle.topol...   \n",
       "181885  topological_vector_bundle.trivial_bundle.topol...   \n",
       "181886  topological_vector_bundle.trivial_bundle.topol...   \n",
       "\n",
       "                             open_namespaces  \\\n",
       "0                                     buffer   \n",
       "1                                     buffer   \n",
       "2                                     buffer   \n",
       "3                                     buffer   \n",
       "4                                     buffer   \n",
       "...                                      ...   \n",
       "181882  topological_vector_bundle bundle set   \n",
       "181883  topological_vector_bundle bundle set   \n",
       "181884  topological_vector_bundle bundle set   \n",
       "181885  topological_vector_bundle bundle set   \n",
       "181886  topological_vector_bundle bundle set   \n",
       "\n",
       "                                       filename  line  column  \\\n",
       "0                 lean/library/data/buffer.lean    49      30   \n",
       "1                 lean/library/data/buffer.lean    49      11   \n",
       "2                 lean/library/data/buffer.lean    49      13   \n",
       "3                 lean/library/data/buffer.lean    49      32   \n",
       "4                 lean/library/data/buffer.lean    49       4   \n",
       "...                                         ...   ...     ...   \n",
       "181882  mathlib/src/topology/vector_bundle.lean   238      60   \n",
       "181883  mathlib/src/topology/vector_bundle.lean   238      60   \n",
       "181884  mathlib/src/topology/vector_bundle.lean   238      51   \n",
       "181885  mathlib/src/topology/vector_bundle.lean   238      51   \n",
       "181886  mathlib/src/topology/vector_bundle.lean   239       5   \n",
       "\n",
       "                                             proof_key  \\\n",
       "0                   lean/library/data/buffer.lean:49:1   \n",
       "1                   lean/library/data/buffer.lean:49:1   \n",
       "2                   lean/library/data/buffer.lean:49:1   \n",
       "3                   lean/library/data/buffer.lean:49:1   \n",
       "4                   lean/library/data/buffer.lean:49:1   \n",
       "...                                                ...   \n",
       "181882  mathlib/src/topology/vector_bundle.lean:237:21   \n",
       "181883  mathlib/src/topology/vector_bundle.lean:238:48   \n",
       "181884  mathlib/src/topology/vector_bundle.lean:237:21   \n",
       "181885  mathlib/src/topology/vector_bundle.lean:238:48   \n",
       "181886  mathlib/src/topology/vector_bundle.lean:237:21   \n",
       "\n",
       "                                        human_tactic_code tactic_class  \\\n",
       "0       cases b; unfold read read'; simp [array.read_e...    semicolon   \n",
       "1                              cases b; unfold read read'    semicolon   \n",
       "2                                       unfold read read'        named   \n",
       "3                              simp [array.read_eq_read']        named   \n",
       "4                                                 cases b        named   \n",
       "...                                                   ...          ...   \n",
       "181882                                               refl        named   \n",
       "181883                                               refl        named   \n",
       "181884                                    { ext x, refl }       solve1   \n",
       "181885                                    { ext x, refl }       solve1   \n",
       "181886  simp only [total_space.topological_space, indu...        named   \n",
       "\n",
       "                                             cleaned_goal  split  \n",
       "0       α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...   test  \n",
       "1       α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...   test  \n",
       "2       α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :...   test  \n",
       "3       α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :...   test  \n",
       "4       α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...   test  \n",
       "...                                                   ...    ...  \n",
       "181882  R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...  train  \n",
       "181883  R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...  train  \n",
       "181884  R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...  train  \n",
       "181885  R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...  train  \n",
       "181886  R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...  train  \n",
       "\n",
       "[181887 rows x 12 columns]"
      ],
      "text/html": "<div>\n<style scoped>\n    .dataframe tbody tr th:only-of-type {\n        vertical-align: middle;\n    }\n\n    .dataframe tbody tr th {\n        vertical-align: top;\n    }\n\n    .dataframe thead th {\n        text-align: right;\n    }\n</style>\n<table border=\"1\" class=\"dataframe\">\n  <thead>\n    <tr style=\"text-align: right;\">\n      <th></th>\n      <th>Unnamed: 0</th>\n      <th>goal_pp</th>\n      <th>decl_name</th>\n      <th>open_namespaces</th>\n      <th>filename</th>\n      <th>line</th>\n      <th>column</th>\n      <th>proof_key</th>\n      <th>human_tactic_code</th>\n      <th>tactic_class</th>\n      <th>cleaned_goal</th>\n      <th>split</th>\n    </tr>\n  </thead>\n  <tbody>\n    <tr>\n      <th>0</th>\n      <td>0</td>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n      <td>buffer.read_eq_read'</td>\n      <td>buffer</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>30</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>cases b; unfold read read'; simp [array.read_e...</td>\n      <td>semicolon</td>\n      <td>α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...</td>\n      <td>test</td>\n    </tr>\n    <tr>\n      <th>1</th>\n      <td>1</td>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n      <td>buffer.read_eq_read'</td>\n      <td>buffer</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>11</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>cases b; unfold read read'</td>\n      <td>semicolon</td>\n      <td>α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...</td>\n      <td>test</td>\n    </tr>\n    <tr>\n      <th>2</th>\n      <td>2</td>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...</td>\n      <td>buffer.read_eq_read'</td>\n      <td>buffer</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>13</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>unfold read read'</td>\n      <td>named</td>\n      <td>α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :...</td>\n      <td>test</td>\n    </tr>\n    <tr>\n      <th>3</th>\n      <td>3</td>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\ni b_fst :...</td>\n      <td>buffer.read_eq_read'</td>\n      <td>buffer</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>32</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>simp [array.read_eq_read']</td>\n      <td>named</td>\n      <td>α : Type u,\\t_inst_1 : inhabited α,\\ti b_fst :...</td>\n      <td>test</td>\n    </tr>\n    <tr>\n      <th>4</th>\n      <td>4</td>\n      <td>α : Type u,\\n_inst_1 : inhabited α,\\nb : buffe...</td>\n      <td>buffer.read_eq_read'</td>\n      <td>buffer</td>\n      <td>lean/library/data/buffer.lean</td>\n      <td>49</td>\n      <td>4</td>\n      <td>lean/library/data/buffer.lean:49:1</td>\n      <td>cases b</td>\n      <td>named</td>\n      <td>α : Type u,\\t_inst_1 : inhabited α,\\tb : buffe...</td>\n      <td>test</td>\n    </tr>\n    <tr>\n      <th>...</th>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n      <td>...</td>\n    </tr>\n    <tr>\n      <th>181882</th>\n      <td>181882</td>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>topological_vector_bundle.trivial_bundle.topol...</td>\n      <td>topological_vector_bundle bundle set</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>60</td>\n      <td>mathlib/src/topology/vector_bundle.lean:237:21</td>\n      <td>refl</td>\n      <td>named</td>\n      <td>R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...</td>\n      <td>train</td>\n    </tr>\n    <tr>\n      <th>181883</th>\n      <td>181883</td>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>topological_vector_bundle.trivial_bundle.topol...</td>\n      <td>topological_vector_bundle bundle set</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>60</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:48</td>\n      <td>refl</td>\n      <td>named</td>\n      <td>R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...</td>\n      <td>train</td>\n    </tr>\n    <tr>\n      <th>181884</th>\n      <td>181884</td>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>topological_vector_bundle.trivial_bundle.topol...</td>\n      <td>topological_vector_bundle bundle set</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>51</td>\n      <td>mathlib/src/topology/vector_bundle.lean:237:21</td>\n      <td>{ ext x, refl }</td>\n      <td>solve1</td>\n      <td>R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...</td>\n      <td>train</td>\n    </tr>\n    <tr>\n      <th>181885</th>\n      <td>181885</td>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>topological_vector_bundle.trivial_bundle.topol...</td>\n      <td>topological_vector_bundle bundle set</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>238</td>\n      <td>51</td>\n      <td>mathlib/src/topology/vector_bundle.lean:238:48</td>\n      <td>{ ext x, refl }</td>\n      <td>solve1</td>\n      <td>R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...</td>\n      <td>train</td>\n    </tr>\n    <tr>\n      <th>181886</th>\n      <td>181886</td>\n      <td>R : Type u_1,\\nB : Type u_2,\\nF : Type u_3,\\n_...</td>\n      <td>topological_vector_bundle.trivial_bundle.topol...</td>\n      <td>topological_vector_bundle bundle set</td>\n      <td>mathlib/src/topology/vector_bundle.lean</td>\n      <td>239</td>\n      <td>5</td>\n      <td>mathlib/src/topology/vector_bundle.lean:237:21</td>\n      <td>simp only [total_space.topological_space, indu...</td>\n      <td>named</td>\n      <td>R : Type u_1,\\tB : Type u_2,\\tF : Type u_3,\\t_...</td>\n      <td>train</td>\n    </tr>\n  </tbody>\n</table>\n<p>181887 rows × 12 columns</p>\n</div>"
     },
     "metadata": {},
     "execution_count": 14
    }
   ],
   "source": [
    "data_and_metadata = pd.read_csv(DATA_DIRECTORY / \"cleaned_training_data\" / \"data_and_metadata.csv\")\n",
    "data_and_metadata"
   ]
  },
  {
   "source": [
    "For each of train, valid, and test there are seperate files:"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "source": [
    "`train.src` is the source (input) data for training (one training example per line)."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "[\"α : Type u,\\tb : buffer α,\\ti : ℕ,\\th : i < b.size,\\tv : α\\t⊢ b.write ⟨i, h⟩ v = b.write' i v\\n\",\n",
       " \"α : Type u,\\tb : buffer α,\\ti : ℕ,\\th : i < b.size,\\tv : α\\t⊢ b.write ⟨i, h⟩ v = b.write' i v\\n\",\n",
       " \"α : Type u,\\ti : ℕ,\\tv : α,\\tb_fst : ℕ,\\tb_snd : array b_fst α,\\th : i < buffer.size ⟨b_fst, b_snd⟩\\t⊢ buffer.write ⟨b_fst, b_snd⟩ ⟨i, h⟩ v = buffer.write' ⟨b_fst, b_snd⟩ i v\\n\",\n",
       " \"α : Type u,\\ti : ℕ,\\tv : α,\\tb_fst : ℕ,\\tb_snd : array b_fst α,\\th : i < buffer.size ⟨b_fst, b_snd⟩\\t⊢ ⟨b_fst, b_snd.write ⟨i, h⟩ v⟩ = ⟨b_fst, b_snd.write' i v⟩\\n\",\n",
       " \"α : Type u,\\tb : buffer α,\\ti : ℕ,\\th : i < b.size,\\tv : α\\t⊢ b.write ⟨i, h⟩ v = b.write' i v\\n\",\n",
       " 'α : Type,\\tp : parser α\\t⊢ ∀ (x : char_buffer), p.bind parser.pure x = p x\\n',\n",
       " 'α : Type,\\tp : parser α\\t⊢ p.bind parser.pure = p\\n',\n",
       " 'α : Type,\\tp : parser α,\\tinput : char_buffer\\t⊢ ∀ (x : ℕ), p.bind parser.pure input x = p input x\\n',\n",
       " 'α : Type,\\tp : parser α,\\tinput : char_buffer\\t⊢ p.bind parser.pure input = p input\\n',\n",
       " 'α : Type,\\tp : parser α,\\tinput : char_buffer,\\tpos : ℕ\\t⊢ p.bind parser.pure input pos = p input pos\\n']"
      ]
     },
     "metadata": {},
     "execution_count": 15
    }
   ],
   "source": [
    "with (DATA_DIRECTORY / \"cleaned_training_data\" / \"train.src\").open() as f:\n",
    "    train_src = list(f)\n",
    "train_src[:10]"
   ]
  },
  {
   "source": [
    "`train.tgt` is the target (output) data for training (one training example per line)."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "[\"cases b; unfold write write'; simp [array.write_eq_write']\\n\",\n",
       " \"cases b; unfold write write'\\n\",\n",
       " \"unfold write write'\\n\",\n",
       " \"simp [array.write_eq_write']\\n\",\n",
       " 'cases b\\n',\n",
       " 'intro input\\n',\n",
       " 'apply funext\\n',\n",
       " 'intro pos\\n',\n",
       " 'apply funext\\n',\n",
       " 'dunfold parser.bind\\n']"
      ]
     },
     "metadata": {},
     "execution_count": 16
    }
   ],
   "source": [
    "with (DATA_DIRECTORY / \"cleaned_training_data\" / \"train.tgt\").open() as f:\n",
    "    train_tgt = list(f)\n",
    "train_tgt[:10]"
   ]
  },
  {
   "source": [
    "`train.names` includes all declaration (theorem) names used for splitting the data."
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "['urysohns.CU.approx_mem_Icc_right_left urysohns.CU urysohns filter topological_space set\\n',\n",
       " 'urysohns.CU.approx_le_succ urysohns.CU urysohns filter topological_space set\\n',\n",
       " 'urysohns.CU.lim_of_mem_C urysohns.CU urysohns filter topological_space set\\n',\n",
       " 'urysohns.CU.lim_of_nmem_U urysohns.CU urysohns filter topological_space set\\n',\n",
       " 'urysohns.CU.lim_eq_midpoint urysohns.CU urysohns filter topological_space set\\n',\n",
       " 'urysohns.CU.continuous_lim urysohns.CU urysohns filter topological_space set\\n',\n",
       " 'topological_vector_bundle.trivialization.continuous_linear_equiv_at topological_vector_bundle bundle set\\n',\n",
       " \"topological_vector_bundle.trivialization.continuous_linear_equiv_at_apply' topological_vector_bundle bundle set\\n\",\n",
       " 'topological_vector_bundle.trivial_bundle_trivialization topological_vector_bundle bundle set\\n',\n",
       " 'topological_vector_bundle.trivial_bundle.topological_vector_bundle topological_vector_bundle bundle set\\n']"
      ]
     },
     "metadata": {},
     "execution_count": 17
    }
   ],
   "source": [
    "with (DATA_DIRECTORY / \"cleaned_training_data\" / \"train.names\").open() as f:\n",
    "    train_names = list(f)\n",
    "train_names[-10:]"
   ]
  },
  {
   "source": [
    "`train.index` contains identifiers for each datapoint (based on the source and declaration name).  _Warning: These identifiers may not be unique._"
   ],
   "cell_type": "markdown",
   "metadata": {}
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {
    "tags": []
   },
   "outputs": [
    {
     "output_type": "execute_result",
     "data": {
      "text/plain": [
       "['{\"src\": \"\\\\u03b1 : Type u,\\\\tb : buffer \\\\u03b1,\\\\ti : \\\\u2115,\\\\th : i < b.size,\\\\tv : \\\\u03b1\\\\t\\\\u22a2 b.write \\\\u27e8i, h\\\\u27e9 v = b.write\\' i v\", \"decl_nm\": \"buffer.write_eq_write\\'\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type u,\\\\tb : buffer \\\\u03b1,\\\\ti : \\\\u2115,\\\\th : i < b.size,\\\\tv : \\\\u03b1\\\\t\\\\u22a2 b.write \\\\u27e8i, h\\\\u27e9 v = b.write\\' i v\", \"decl_nm\": \"buffer.write_eq_write\\'\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type u,\\\\ti : \\\\u2115,\\\\tv : \\\\u03b1,\\\\tb_fst : \\\\u2115,\\\\tb_snd : array b_fst \\\\u03b1,\\\\th : i < buffer.size \\\\u27e8b_fst, b_snd\\\\u27e9\\\\t\\\\u22a2 buffer.write \\\\u27e8b_fst, b_snd\\\\u27e9 \\\\u27e8i, h\\\\u27e9 v = buffer.write\\' \\\\u27e8b_fst, b_snd\\\\u27e9 i v\", \"decl_nm\": \"buffer.write_eq_write\\'\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type u,\\\\ti : \\\\u2115,\\\\tv : \\\\u03b1,\\\\tb_fst : \\\\u2115,\\\\tb_snd : array b_fst \\\\u03b1,\\\\th : i < buffer.size \\\\u27e8b_fst, b_snd\\\\u27e9\\\\t\\\\u22a2 \\\\u27e8b_fst, b_snd.write \\\\u27e8i, h\\\\u27e9 v\\\\u27e9 = \\\\u27e8b_fst, b_snd.write\\' i v\\\\u27e9\", \"decl_nm\": \"buffer.write_eq_write\\'\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type u,\\\\tb : buffer \\\\u03b1,\\\\ti : \\\\u2115,\\\\th : i < b.size,\\\\tv : \\\\u03b1\\\\t\\\\u22a2 b.write \\\\u27e8i, h\\\\u27e9 v = b.write\\' i v\", \"decl_nm\": \"buffer.write_eq_write\\'\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type,\\\\tp : parser \\\\u03b1\\\\t\\\\u22a2 \\\\u2200 (x : char_buffer), p.bind parser.pure x = p x\", \"decl_nm\": \"parser.parser.id_map\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type,\\\\tp : parser \\\\u03b1\\\\t\\\\u22a2 p.bind parser.pure = p\", \"decl_nm\": \"parser.parser.id_map\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type,\\\\tp : parser \\\\u03b1,\\\\tinput : char_buffer\\\\t\\\\u22a2 \\\\u2200 (x : \\\\u2115), p.bind parser.pure input x = p input x\", \"decl_nm\": \"parser.parser.id_map\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type,\\\\tp : parser \\\\u03b1,\\\\tinput : char_buffer\\\\t\\\\u22a2 p.bind parser.pure input = p input\", \"decl_nm\": \"parser.parser.id_map\"}\\n',\n",
       " '{\"src\": \"\\\\u03b1 : Type,\\\\tp : parser \\\\u03b1,\\\\tinput : char_buffer,\\\\tpos : \\\\u2115\\\\t\\\\u22a2 p.bind parser.pure input pos = p input pos\", \"decl_nm\": \"parser.parser.id_map\"}\\n']"
      ]
     },
     "metadata": {},
     "execution_count": 18
    }
   ],
   "source": [
    "with (DATA_DIRECTORY / \"cleaned_training_data\" / \"train.index\").open() as f:\n",
    "    train_index = list(f)\n",
    "train_index[:10]"
   ]
  }
 ]
}