no goals
𝕜 : Type ?u.84393
E : Type u_1
F : Type ?u.84399
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
hs : Balanced ℝ s
x : E
hx : x ∈ s
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ ‖a‖ ≤ 1
rwa [Real.norm_of_nonneg ha₀]