You can use existsi instead of use.

How do I avoid error messages like this one when working with large (say 10 digit) numbers?

deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

Turns out I had to import tactic first. Now it works.

I'm new to Lean Codewars. I'm used to fill ∃ quantifiers with the use tactic, but the Codewars Lean doesn't seem to know it:

Solution.lean:3:4
unknown identifier 'use'
Solution.lean:3:4
don't know how to synthesize placeholder
context:
⊢ Type ?

How do I solve such a kata here on Codewars? My code works in my "regular" Lean environment.