no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.36800
G : Type ?u.36803
ι : Type ?u.36806
π : ι → Type ?u.36811
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x✝¹ y z✝ x z : E
x✝ : z ∈ [x-[𝕜]x]
a b : 𝕜
w✝¹ : 0 ≤ a
w✝ : 0 ≤ b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}
simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz