apply (affineSpan_mono _ hst.subset).lt_of_ne
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
⊢ affineSpan ℝ t < affineSpan ℝ s
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
s t C : Set E
X : Finset E
l : E →L[ℝ] ℝ
hst : IsExposed ℝ s t
hts : ¬s ⊆ t
⊢ affineSpan ℝ t ≠ affineSpan ℝ s