Here we include a dump of proofs in coq-gym using the proverbot9001 tool.
relevant_lemmas: A list of lemmas that are relevant to the proof. Each lemma is accompanied by its formal statement and registration in the proof context.
prev_tactics: The tactics used in the previous steps of the proof (The first tactic being the lemma definition itself). This can help in understanding the sequence of operations leading to the current… See the full description on the dataset page:
https://huggingface.co/datasets/brando/Coq-Gym-Data-Set.
