obtain ⟨ε, hε, hεx⟩ := (Metric.nhds_basis_closedBall.1 _).1 (isOpen_iff_mem_nhds.1 hs _ hx)
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s