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
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
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
f : Finset (Fin (finrank ℝ ↥(vectorSpan ℝ s))) → ↥(vectorSpan ℝ s) :=
  fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
hf :
  f = fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s