[Merged by Bors] - chore: use IsScalarTower.algebraMap_eq to golf two proofs#33353

ocfnash wants to merge 5 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

ocfnash:ocfnash/algebraMap_towerocfnash/mathlib4:ocfnash/algebraMap_towerCopy head branch name to clipboard