chore(algebra/lie/basic + classical): golf some proofs (#7903)
Another PR with some golfing, to get acquainted with the files! Oliver, I really like how you set this up!
Also, feel free to say that you do not like the golfing: there is a subtle tension between proving stuff fast and making it accessible!
