LeanDojo's REPL/ExtractData.lean and mods to REPL/Main.lean to populate AST

[vadimkantorov]

• this patch is taken from master...xinhjBrant:repl:deepseek - minorly updated by me to apply to the recent main branch of REPL
• which claims it comes from LeanDojo's https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean

This REPL fork is used for https://github.com/Goedel-LM/Goedel-Prover, so I wonder if it's useful in general for similar work

I also wonder if test inputs/outputs then would be needed to updated (at least to include a placeholder for empty ast field in the outputs)

I'm not understanding enough of whether it's useful to have it upstream, so please feel free to close or edit

[kim-em]

There is a lot of code here that is duplicated with existing code elsewhere in the REPL. Can you please fix this before we review it?