classical
lift x to affineSpan ℝ s using subset_affineSpan _ _ hx
set x : affineSpan ℝ s := x with hx
clear_value x
subst hx
obtain ⟨ε, hε, hεx⟩ := (Metric.nhds_basis_closedBall.1 _).1 (isOpen_iff_mem_nhds.1 hs _ hx)
set f : Finset (Fin $ finrank ℝ $ vectorSpan ℝ s) → vectorSpan ℝ s :=
  fun u ↦ (ε / ∑ i, ‖finBasis ℝ (vectorSpan ℝ s) i‖) • ∑ i, if i ∈ u then
    finBasis ℝ (vectorSpan ℝ s) i else -finBasis ℝ (vectorSpan ℝ s) i
    with hf
sorry
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : IsOpen (Subtype.val ⁻¹' s)
hx : x ∈ s
⊢ ∃ t, x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
no goals