refactor(analysis/normed_space/operator_norm): split a proof (#11112)
refactor(analysis/normed_space/operator_norm): split a proof (#11112)

Split the proof of `continuous_linear_map.complete_space` into
reusable steps.

Motivated by #9862





leanprover-community/mathlib,leanprover-community/mathlib