A CAS also covers only a tiny part of "an undergrad math degree" so that's beside the point here. Assuming it had appropriate tactics doing the job of a CAS using all theorems (which isn't happening any time soon), what math would be missing?

I'm not really sure what you're asking. I wasn't commenting on any of the CAS asoects of Lean or Mathlib.

> what math would be missing

Just generally speaking, manifolds. There's no clear or standard approach in Mathlib. There seem to be approaches, but they definitely aren't turnkey.