Natural Deduction

Stream: new members

[Eduardo Ochs]

Hi, I started learning Lean 10 days ago, and one of the things that I'm doing to try to understand the tactics is this improvised translation of the exercises in the Natural Numbers Game to Natural Deduction...

http://angg.twu.net/LATEX/2021lean-nng.pdf

Is there an official, i.e., non-improvised, way to do this?
addition-world-1-6-nd.png

[Alex J. Best]

There is docs#tactic.explode which might do something like what you want?

[Eduardo Ochs]

YES!!!!! Thanks! =)