I started one such tutorial: https://agentultra.github.io/lean-for-hackers/

I haven't gotten to the dependent types part yet. I find most tutorials one these languages start with the theory up front. I'm taking a more pragmatic tack by demonstrating the language through examples building on familiar learning patterns of writing simple programs first and working your way up.

It is a neat way to write programs!