In the [proof of Banach-Steinhaus in 12.2.2](https://github.com/avigad/mathematics_in_lean_source/blob/8baa112dcb882785255fdcb6aee4cac88a0c4925/MIL/C12_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean#L223), the comment "`e m` contains some `x`" should be changed to "the interior of `e m` contains some `x`".
In the proof of Banach-Steinhaus in 12.2.2, the comment "
e mcontains somex" should be changed to "the interior ofe mcontains somex".