no goals
ι : Type ?u.124932
𝕜 : 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 : x + y ∈ interior s
t : 𝕜
ht : t ∈ Ioc 0 1
⊢ x + t • y ∈ interior s
simpa only [add_sub_cancel'] using hs.add_smul_sub_mem_interior' hx hy ht