chore: use new elaborators more

[grunweg]

• depends on: mathlib4#30413
• further use will need
  • a fix in the elaborators: if E is a real inner product space, we don't find the trivial model yet (even though InnerProductSpace implies NormedSpace)
  • an extension for finding the model on OneJetBundle... perhaps when this is an environment extension, so can be don here also