Commit 2021-07-10 08:01 b1806d19

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.