Create a new lean file with the name specified below in Game/Levels/content_drafts which correctly compiles and defines and proves the theorem below.
Break into intermediate theorems/lemmas if necessary (to go into separate levels, or provided as 'given' helpers, tbd later).
There's a decent variety of lean and a non-trivial calc-block.
Curious about how this will play out in the browser.
This might have to be split into several levels.
Game/Levels/content_drafts
which correctly compiles and defines and proves the theorem below. Break into intermediate theorems/lemmas if necessary (to go into separate levels, or provided as 'given' helpers, tbd later).metric_wrld_L03.lean
Syllabus outline: #5