-- Mathlib/Analysis/Convex/Caratheodory.lean
theorem convexHull_eq_union : convexHull 𝕜 s =
    ⋃ (t : Finset E) (_ : ↑t ⊆ s) (_ : AffineIndependent 𝕜 ((↑) : t → E)), convexHull 𝕜 ↑t

Proof state:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s = ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t

Tactic:
apply Set.Subset.antisymm

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

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

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

Tactic:
intro x hx

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

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

Tactic:
iterate 3 convert Set.iUnion_subset _; intro

Result:
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 𝕜) ↑i✝² ⊆ (convexHull 𝕜) s

Proof state:
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 𝕜) ↑i✝¹ ⊆ (convexHull 𝕜) s

Tactic:
convert Set.iUnion_subset _

Result:
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 𝕜) ↑i✝¹ ⊆ (convexHull 𝕜) s

Proof state:
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 𝕜) ↑i✝² ⊆ (convexHull 𝕜) s

Tactic:
exact convexHull_mono ‹_›

Result:
no goals

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

Tactic:
simp only [exists_prop, Set.mem_iUnion]

Result:
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ (convexHull 𝕜) ↑i

Proof state:
case h₁
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ (convexHull 𝕜) s
⊢ ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ (convexHull 𝕜) ↑i

Tactic:
exact ⟨Caratheodory.minCardFinsetOfMemConvexHull hx,
  Caratheodory.minCardFinsetOfMemConvexHull_subseteq hx,
  Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull hx,
  Caratheodory.mem_minCardFinsetOfMemConvexHull hx⟩

Result:
no goals

Proof state:
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 𝕜) ↑i✝¹ ⊆ (convexHull 𝕜) s

Tactic:
intro

Result:
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 𝕜) ↑i✝² ⊆ (convexHull 𝕜) s