Theorem: ConvexIndependent.subset_of_convexHull_eq_convexHull (LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
⊢ s ⊆ t
Tactic:
rintro x hx
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
⊢ x ∈ t

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
⊢ x ∈ t
Tactic:
have hxextreme := (extremePoints_convexHull_eq_iff_convexIndependent.2 hs).symm.subset hx
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
hxextreme : x ∈ extremePoints 𝕜 ((convexHull 𝕜) fun x => x ∈ s.val)
⊢ x ∈ t

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
hxextreme : x ∈ extremePoints 𝕜 ((convexHull 𝕜) fun x => x ∈ s.val)
⊢ x ∈ t
Tactic:
erw [h] at hxextreme
State after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
hxextreme : x ∈ extremePoints 𝕜 ((convexHull 𝕜) ↑t)
⊢ x ∈ t

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ t✝ : Set E
x✝ : E
s t : Finset E
hs : ConvexIndependent 𝕜 Subtype.val
h : (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑t
x : E
hx : x ∈ s
hxextreme : x ∈ extremePoints 𝕜 ((convexHull 𝕜) ↑t)
⊢ x ∈ t
Tactic:
exact_mod_cast extremePoints_convexHull_subset hxextreme
State after:
no goals