case h.e'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.183431
G : Type ?u.183434
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ {t | s ⊆ ↑t} = {t | ↑(convexHull 𝕜).toOrderHom s ⊆ ↑t}
𝕜 : Type u_2
E : Type u_1
F : Type ?u.183431
G : Type ?u.183434
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ IsLeast {t | s ⊆ ↑t} (Convex.toCone (↑(convexHull 𝕜).toOrderHom s) (_ : Convex 𝕜 (↑(convexHull 𝕜).toOrderHom s)))
convert (convex_convexHull 𝕜 s).toCone_isLeast using 1
case h.e'_3.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.183431
G : Type ?u.183434
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
t : ConvexCone 𝕜 E
⊢ t ∈ {t | s ⊆ ↑t} ↔ t ∈ {t | ↑(convexHull 𝕜).toOrderHom s ⊆ ↑t}
case h.e'_3
𝕜 : Type u_2
E : Type u_1
F : Type ?u.183431
G : Type ?u.183434
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ {t | s ⊆ ↑t} = {t | ↑(convexHull 𝕜).toOrderHom s ⊆ ↑t}
ext t
no goals
case h.e'_3.h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.183431
G : Type ?u.183434
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
t : ConvexCone 𝕜 E
⊢ t ∈ {t | s ⊆ ↑t} ↔ t ∈ {t | ↑(convexHull 𝕜).toOrderHom s ⊆ ↑t}
exact ⟨fun h => convexHull_min h t.convex, (subset_convexHull 𝕜 s).trans⟩