no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.172872
G : Type ?u.172875
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x✝ x : E
hx : x ∈ s
⊢ 1 • x ∈ s
rwa [one_smul]