no goals
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ‖↑(↑B x✝¹) 0‖ ≤ 1
simp only [map_zero, norm_zero, zero_le_one]