What is the easiest way to prove Char.utf8Size c > 0?

Stream: lean4

[l1mey]

I've been having a hard time so far, I don't really know how to get around the if statement in there nicely.

image.png

[Robin Arnez]

We have docs#Char.utf8Size_pos​..?

[l1mey]

Whoops.

[Robin Arnez]

But it should be enough to simply simp [h1, h2] in your example to solve the goal

[Kim Morrison]

Don't forget to run try? if you're stuck! (For now there's also hint in Mathlib, which I'm intending to roll into try? soon.)