I'm not looking to use it as a programming language, but I'd like to see an introduction to theorem proving using Lean that is more explicit in its explanation of semantics than the ones that assume an existing math background

Theorem Proving in Lean 4: https://leanprover.github.io/theorem_proving_in_lean4/

I only had a basic knowledge of first-order logic and set theory before reading TPiL4. It wasn't easy, but now I can prove theorems in Lean. By the way, I still can't write a program in any language.