Yes split_ifs is in Mathlib so I have replaced it with split (twice) which is in Core. I believe there is also an intermediate level Std. I'm not sure why you'd want to avoid Mathlib but I daresay it's possible for many types of problem.
No comments yet.