NFA pumping lemma bound

Stream: mathlib4

[Maja Kądziołka]

while browsing around, I've noticed that NFA.pumping_lemma bounds the minimum length of the string as $2^{|\sigma|}$, while $|\sigma|$ is the optimal bound. would it make sense for me to work on an improved proof for this?

[Yaël Dillies]

Looks like a fine thing to work on to me!

[Maja Kądziołka]

So, looks like I'd want to use something like the IsPath API that's currently available for \epsNFA, but not NFA itself. Mirroring the API here would be desirable, right? I can imagine some ways I could be trying to avoid doing that by proving the pumping lemma for eps-NFAs and then transferring back to normal NFAs (in the opposite direction to what the import hierarchy is doing), but that's not a good idea, is it?