rw [← closure_diff_frontier] at hy ⊢
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ interior s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ interior s
case intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t : Set E
x✝ : E
s : Set E
hAconv : Convex 𝕜 s
x y : E
hy : y ∈ closure s \ frontier s
z : ℕ → E
hzA : ∀ (n : ℕ), z n ∈ s
hzx : Filter.Tendsto z Filter.atTop (nhds x)
n : ℕ
⊢ (fun n => (1 - 1 / (↑n + 2)) • z n + (1 / (↑n + 2)) • y) n ∈ closure s \ frontier s