Honestly, I'd say just play some of the lean games instead (https://adam.math.hhu.de/). I went through the dependent type theory and proof stuff first, and in hindsight it would have been much faster to just get the intuition first from learning to use a language like lean.

You're crazy. Don't bother to try to understand lean's internal models unless you want to work on lean itself. Whatever style of proof you're used to, you can write in that style with mathlib.