I completely agree, this seems significantly easier than some of the other 4-kyu ranked puzzles out there. 6-kyu would seem more adequate.

Same for Coq. As far as I can tell there is no way to inspect the Preloded file, and the interface of codewards is completely inadequate. I managed to find the required definitions by Printing their names and "attempting" to solve the problem, which then shows the result of running the file. But this is really suboptimal.

Edit: Ok, my bad, the definitions are provided in the comments of the problem. This still strikes me as a weird way to do it.

Thank you for the advice! By the way, @mentions do not work on Codewars. I usually check all recent comments at https://www.codewars.com/dashboard. That's how I found your comment. It is possible to write comments directly under solutions. Then solution authors will get comment notifications.

It's a CW bug or something, I just reported it. Did you click Fork? It's crazy x)

Apologies for the blunder, I have edited the links to point to the community resources instead.

I have removed all the unnecessary imports in the Initial Solution - please confirm :-)

Due to the way Lean is set up on Codewars, giving access to earlier parts can only be achieved by providing their proof(s) in Preloaded.lean as well which would spoil the earlier challenges.

As a classical mathematician I would encourage a site policy of allowing noncomputable and nonconstructive proofs of everything and my impression is that this is what you're allowing too because there were no complaints when the classical axioms were detected.

That is true of the current Lean setup on Codewars (but not true for Coq / Idris / Agda), and we do not intend to change that since (as I mentioned on the GitHub issue ticket requesting Lean support on Codewars) our primary aim of adding Lean to Codewars is to diversify our range of theorem-proving challenges to include "fashionable mathematics" and attract mathematicians interested in computerized theorem-proving to join the site and contribute such challenges.

Should it be made clear somewhere that use of LEM and classical arguments more generally is acceptable?

Since this is a site-wide policy (for Lean) and not Kata-specific, I'll mention it on our Wiki page.

You should be able to view submitted solutions to Kata you have completed by selecting the Kata in question and selecting the "Solutions" tab (it's right next to "Discourse"). So, for example, if you have completed #2 and would like to invoke the result in #4 but deleted your solution to #2 locally, you may simply copy (parts of) solutions to #2 in the solutions page.

Thanks for your input! I will definitely change this once I have the time.