All of these things are definitely not necessary to know about to successfully use Lean, and not even useful to know for proving things in Lean.