There is a short one[1] from Functional Programming in Lean, which is itself an introduction to Lean 4 from the programming's perspective. Highly recommended if you're interested in dependent types.

[1]: https://leanprover.github.io/functional_programming_in_lean/...