Questions about data

[yuchen814]

In the corpus.jsonl file, are there cases where some tactics in the train/val/test datasets are not traced? For example, while 'ENNReal.coe_toNNReal' exists in the train/val/test datasets, its 'traced_tactics' field is empty:
{
"url": "/Users/xx/.cache/lean_dojo/leanprover-community-mathlib4-92c2d0cbb4aa68ea1be62aaf7c3517f7f8e1f385/mathlib4",
"commit": "92c2d0cbb4aa68ea1be62aaf7c3517f7f8e1f385",
"file_path": "Mathlib/Data/ENNReal/Basic.lean",
"full_name": "ENNReal.coe_toNNReal",
"start": [194, 1],
"end": [196, 25],
"traced_tactics": []
}
Additionally, I couldn’t find 'Eq.symm' in the train/val/test datasets.

[yangky11]

coe_toNNReal has a term-style proof w/o any tactic.

https://github.com/leanprover-community/mathlib4/blob/94099b4e3e03fbb365bb797d566a2168442c7a34/Mathlib/Data/ENNReal/Basic.lean#L200

Where is Eq.symm defined? If it's in lean4 itself instead of mathlib. It's probably not in the dataset.

[yuchen814]

Thank you very much!