I wouldn't be too surprised if PL proofs were simpler to start with. Part of what I hear people say is that they also are a lot more routine. Do structural induction, apply the IH to show an invariant holds, continue. I haven't done much theorem proving, nor have I done any "mathematical" (e.g. analysis) proofs with a theorem prover, but it makes me wonder how much skill transfer there is between them if "mathematical" proofs require a much different approach.

I will also mention Software Foundations in Rocq (perhaps there is a Lean port). I worked through some of the first parts of it and found it quite pleasant.

Kevin Buzzard said something like the PL proofs are about deep structures on simple objects (mostly integers), while modern math mainly concerns complex objects. If you already have the definitions, the properties usually don't involve a lot of recursion and case analyses.