no goals
ι : Type ?u.112869
𝕜 : Type u_2
E : Type u_1
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ closure s
hy : y ∈ interior s
t : 𝕜
ht : t ∈ Ioc 0 1
⊢ x + t • (y - x) ∈ interior s
simpa only [sub_smul, smul_sub, one_smul, add_sub, add_comm] using
  hs.combo_interior_closure_mem_interior hy hx ht.1 (sub_nonneg.mpr ht.2)
    (add_sub_cancel'_right _ _)