no goals
𝕜 : Type ?u.97683
E : Type u_1
F : Type ?u.97689
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
hs₁ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : ¬x ∈ s
⊢ ¬x ∈ 1 • s
rwa [one_smul]