You need to understand the concept of the core algebra and 100s (with the s), then I think you'd be better positioned to understand my comment.

And granted, I don't know the exact details about Lean. It might be that they don't have an incredibly simple core - as has elsewise been the norm.