Save Context and Goal at Each Step of a Proof in Lean

Stream: general

[White Chen]

In Lean, I want to save the context and goal before and after each step (line?) of a proof. I know that LeanDojo can accomplish this, but it seems not convenient enough. Is there a simpler method to achieve this?

[Jason Rute]

I’ve used https://github.com/semorrison/lean-training-data for this.