Uhh, it is nasty :)

For what it's worth, I proposed this as a 7kyu kata :)
I also agree with the above comment that theorem proving kata can have different sorts of difficulty, but I think this particular one is mathematically fairly straightforward.

I agree with the statement of ipergenitsa above. Perhaps, for Coq and other theorem proving tools, it would be a good idea to differentiate between different aspects of the katas complexity (with a tag ?):

• Program and prove: the main difficulty is to write and prove a program
• Mathematics: the main difficulty is to find the proof in theoretical maths (I mean that translating it into Coq is easy but the reasonning is hard)
• Logicians and tricks of Coq: the main difficulty is to know the very last features of the tool and the exact logic it relies on.

I think this particular problem would fall into the second category meaning that it is significantly harder for someone with a small background in mathematics. I personally struggled with problems of the third category (for example one using the very new feature of polymorphic universes in Coq).
Note that I may have missed the relevant tags and the respective meaning of 8kyu/7kyu etc (pointers are welcome ;) )

I am facing an issue while submitting the solution. Codewars Lean is not at the same state as my own editor when going through the proof. As a result it is not accepting my proof. I have checked that my proof works on my local machine (using Lean 3.8.0) and on the mathlib lean web editor (using Lean 3.9.0). Is the error being caused by CW's lean being at 3.7?

I agree that it should be 7kyu. But as I said, ranks can't be changed. It's 8kyu for non-beginners. ;-)

I would be glad to try this new area (theorem proving) as well as new (non-traditional) programming languages.
My opinion that 8kyu should be like the starting point, shouldn't it? But instead of simple stuff to get in touch with new ideas and approaches, I find hard tasks that forces me to read a book. I would like to see like step by step tasks. Otherwise this becomes very useless when the only people who can solve it the ones who worked with this before

The task was probably ranked without concern for users who have no idea what theorem proving is, also regarding your first sentence, to put it bluntly, no one forces you to do so.

It's totally crazy... I don't want to spend hours reading a text to solve "the easiest" task.
Actually I don't find anything hard in what I read, despite this I cannot solve it. It does not even make me thinking about anything, just getting info...

It's not the author's decision about the rank, and also, they can't be changed.

Are you kidding applying 8kyu to it?
I've read some chapters of this work: https://softwarefoundations.cis.upenn.edu/current/lf-current/toc.html and could not imaging how to prove it.
I've taken a look at lean and it looks even more tricky

Yes.

It can consume huge amount of memory, right?

I don't know why this does not work, maybe the bug is already fixed in the version I use locally.
But I've found another solution that works locally as well as here :)