case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ↑(convexHull 𝕜).toOrderHom s ⊆
    ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜).toOrderHom ↑t

case h₂
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜).toOrderHom ↑t) ⊆
    ↑(convexHull 𝕜).toOrderHom s
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ↑(convexHull 𝕜).toOrderHom s =
    ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜).toOrderHom ↑t
apply Set.Subset.antisymm
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ x ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜).toOrderHom ↑t
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ↑(convexHull 𝕜).toOrderHom s ⊆
    ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜).toOrderHom ↑t
intro x hx
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ ↑(convexHull 𝕜).toOrderHom ↑i
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ x ∈ ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜).toOrderHom ↑t
simp only [exists_prop, Set.mem_iUnion]
no goals
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ↑(convexHull 𝕜).toOrderHom s
⊢ ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ ↑(convexHull 𝕜).toOrderHom ↑i
exact ⟨Caratheodory.minCardFinsetOfMemConvexHull hx,
  Caratheodory.minCardFinsetOfMemConvexHull_subseteq hx,
  Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull hx,
  Caratheodory.mem_minCardFinsetOfMemConvexHull hx⟩
case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝² : Finset E
i✝¹ : ↑i✝² ⊆ s
i✝ : AffineIndependent 𝕜 Subtype.val
⊢ ↑(convexHull 𝕜).toOrderHom ↑i✝² ⊆ ↑(convexHull 𝕜).toOrderHom s
case h₂
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜).toOrderHom ↑t) ⊆
    ↑(convexHull 𝕜).toOrderHom s
iterate 3 convert Set.iUnion_subset _; intro
no goals
case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝² : Finset E
i✝¹ : ↑i✝² ⊆ s
i✝ : AffineIndependent 𝕜 Subtype.val
⊢ ↑(convexHull 𝕜).toOrderHom ↑i✝² ⊆ ↑(convexHull 𝕜).toOrderHom s
exact convexHull_mono ‹_›
case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝¹ : Finset E
i✝ : ↑i✝¹ ⊆ s
⊢ AffineIndependent 𝕜 Subtype.val → ↑(convexHull 𝕜).toOrderHom ↑i✝¹ ⊆ ↑(convexHull 𝕜).toOrderHom s
case h₂.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝¹ : Finset E
i✝ : ↑i✝¹ ⊆ s
⊢ (⋃ (_ : AffineIndependent 𝕜 Subtype.val), ↑(convexHull 𝕜).toOrderHom ↑i✝¹) ⊆ ↑(convexHull 𝕜).toOrderHom s
convert Set.iUnion_subset _
case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝² : Finset E
i✝¹ : ↑i✝² ⊆ s
i✝ : AffineIndependent 𝕜 Subtype.val
⊢ ↑(convexHull 𝕜).toOrderHom ↑i✝² ⊆ ↑(convexHull 𝕜).toOrderHom s
case h₂.convert_5.convert_5.convert_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
i✝¹ : Finset E
i✝ : ↑i✝¹ ⊆ s
⊢ AffineIndependent 𝕜 Subtype.val → ↑(convexHull 𝕜).toOrderHom ↑i✝¹ ⊆ ↑(convexHull 𝕜).toOrderHom s
intro