Theorem: IsExposed.span_lt (LeanCamCombi/Mathlib/Analysis/Convex/Exposed.lean)

State before:
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
Tactic:
apply (affineSpan_mono _ hst.subset).lt_of_ne
State after:
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

State before:
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
Tactic:
rintro h
State after:
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
h : affineSpan ℝ t = affineSpan ℝ s
⊢ False

State before:
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
h : affineSpan ℝ t = affineSpan ℝ s
⊢ False
Tactic:
sorry
State after:
no goals