I can reproduce. This is hard to debug without having access to the exact contents of Preloaded.lean [do I have access to this file?]

I made a solution in VS Code (Lean 3.7.2) but it doesn't work on this site. Could there be some subtle difference between the contents of the Preloaded import and the definitions commented out in the answer template?

What is the point of n? Why not just ask to prove empty_place t = node t + 1?

Approved, thanks!

I learned a lot by doing this, thank you!
Personally I found it a bit hard, I'd say harder than the Google interview.

Fixed, thanks:-)

Thanks for the clarification.

A nitpick - since a binary tree could have multiple "empty place"s, would it make more sense to edit the Description to say (emphasis mine):

And here is a function to calculate an empty place that can insert a node on a tree.

instead of:

And here is a function to calculate the empty place that can insert a node on a tree.

?

Cheers :-)

As a side note, not directly related to this Kata but be sure to check out other Coq Kata currently in the Beta phase as well (-: For each Beta Kata that you complete, don't forget to give your satisfaction vote and ranking vote as well - they are key in helping them getting approved (like what happened to this Kata - the Kata exits the Beta phase and is given an official ranking, e.g. 7 kyu) which gives the Kata author and every Codewarrior who solved the Kata rank progress and additional honor. Happy sparring! ^_^

Well, the empty place is where you can insert a node while it remains a binary tree, for example, a leaf may have two empty places.

I'm not quite sure I understand what is meant by "empty place" as described in this Kata, would you mind elaborating?

Approved ;-)

Well done on authoring your first Coq Kata on Codewars, looking forward to more Coq Kata authored by you