mathlib

06c55940 - chore(analyis/normed_space/banach): split proof to avoid timeout (#2053)

chore(analyis/normed_space/banach): split proof to avoid timeout (#2053) * chore(analyis/normed_space/banach): split proof to avoid timeout * delay introducing unnecessary variable * Apply suggestions from code review Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * fix indent Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>