chore(analysis/normed_space/banach): speed up the proof (#8230)
This proof has timed out in multiple refactor PRs I've made. This splits out an auxiliary definition.
The new definition takes about 3.5s to elaborate, and the two lemmas are <500ms each.
The old lemma took 45s.
Co-authored-by: Johan Commelin <johan@commelin.net>
