If this comment is addressed to me, I am not sure I am confident enough with Coq syntax any more to know whether what you have done is OK (I haven't used Coq for about 2 years and I quickly forget things which I don't use a lot).

Either there is some issue with imports (the most likely -- even should be defined in preloaded) or there's a difference between Lean 3.5.1 (CoCalc) and Lean 3.7.2 (here) but that is vanishingly unlikely with kata at this level (cutting edge mathlib stuff changes but not basic stuff like this).

Edit: Oh, but I see you solved it :-)

@monadius : rw X at this, exact this can be abbreviated to rwa X at this; rwa := rw, assumption. Normally rwa is used when the goal can be rewritten to an assumption but this variant also works.

The description claims that SL_2(N) is a group. Not so (no inverses). It might also be worth mentioning that the description defines SL_2(N) as being {(a,b,c,d) : ad-bc=1} but the actual definition is completely different. One could beef this kata up by asking to prove that evaluation is a bijection from the free monoid SL₂ℕ to the matrices with ad-bc=1, rather than just an injection to the type of all natural number matrices.

Ooh yes thanks.

PS I wouldn't bother with the mutual types -- I think the set-up here is fine.

This is type theory 101 in the CS courses, see for example https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab207 . I don't think you need examples.

Suggestions:

I would call the even_succ constructor even_ss following software foundations, and similarly odd_ss. The standard mathlib names for your lemmas would be something like this: even_plus_one_is_odd -> odd_add_one, odd_plus_one_is_even -> even_add_one, every_number_is_odd_or_even -> odd_or_even, odd_plus_odd_is_even -> odd_add_odd, odd_plus_even_is_odd -> even_add_odd etc, even_times_even_is_even -> even_mul_even etc and even_times_anything_is_even -> even_mul. Finally, a lot of the variables should be implicit: whenever you have an assumption (n) (hn : even n) the n should be {n}; this applies to odd_add_one etc, odd_add_odd etc and even_mul_even etc.

Not if (1+2+...+n) is embedded in the middle of a more complex term, for example (3+n^2)*(5+(1+2+...+n)). Multplying the sum by 2 is a pain.

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?]

How come one of the solutions has a sorry?

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