no goals
V : Type u_1
P : Type ?u.126361
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ Set.Nonempty (interior s) ↔ affineSpan ℝ s = ⊤
rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]