clear_value x
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)
x : ↥(affineSpan ℝ s) := x✝
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ x : ↥(affineSpan ℝ s)
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s