Conventions regarding length in lists

Stream: new members

[Kati Overbeeke]

Hi, I started using Lean a few months ago and I am proving a theorem where I need to index lists, I currently have either help lemmas or help hypothesis or using the '(by ... proof) functionality all together and I was wondering if there are conventions for this. Furthermore, are there also conventions when this happens in a theorem? Do you add this as an assumption in the theorem?