The definition is monstrous when unfolded, but luckily Lean's rewrite matches the huge expressions masterfully and does unification automatically so that the induction hypothesis is applied correctly, as in my solution (rw ih): https://www.codewars.com/kumite/5f2e30269de164002a276bd0?sel=5f2e303cf51db50010b60b36

Using gas instead of well-founded recursion is fine and preserves the original intent of the problem. But using recursors (nat.rec_on, etc.) directly is not idiomatic in Lean (or in any other theorem prover as far as I know). Using the equation compiler even for structural recursion makes a difference in Lean because it causes equational lemmas to be generated.

I don't want to change definitions in this kata but I'm going to update my other kata and use well-founded recursion in Lean there.

A citation from Codewars wiki: "A translation is essentially just a "port" of the original kata to a new language. Every aspect of the original kata should be retained." It is not enforced but it is a good practice to keep all translations consistent. I consider the original definition to be important so I don't want to change the Lean version. The original intention of the kata is the following: Verify that the given program is correct. It is wrong to change the program in Lean only because there is another way to write the same program.

It is definitely possible. But the original version of this kata is done in Idris where the current definition is much simpler than a definition based on well-founded recursion. All translations faithfully preserved the original definition.