Add ability to toggle between rendered view and literal lean

[al-yisun]

In my case I have looked up actual lean files elsewhere, but it would be nice while learning if each problem/solution could be viewed as a lean source file which could literally be run in an interpreter with the relevant imports and instruction text as comments. Perhaps a toggle back and forth?