Does LeanDojo support for whole proof evaluation instead of a single tactic?

[zengyuzhi]

Same as title

[yangky11]

Actually I'm not quite sure what will happen if you enter the entire proof into LeanDojo. It should be possible to break the proof into a sequence of tactics (term-style proofs can be converted by adding the exact tactic)?

Maybe it's helpful to discuss a few concrete examples.

[zengyuzhi]

Thank you for you help!