-- Mathlib/Analysis/Convex/Caratheodory.lean
theorem eq_pos_convex_span_of_mem_convexHull {x : E} (hx : x ∈ convexHull 𝕜 s) :
    ∃ (ι : Sort (u + 1)) (_ : Fintype ι),
      ∃ (z : ι → E) (w : ι → 𝕜), Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ i, 0 < w i) ∧
        ∑ i, w i = 1 ∧ ∑ i, w i • z i = x

Proof state:
case intro.intro.intro.intro.intro.intro.refine_1
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ {x | x ∈ t'} ⊆ s

Tactic:
exact Subset.trans (Finset.filter_subset _ t) ht₁

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ x ∈ t, w x • x = x

Tactic:
rw [t.centerMass_eq_of_sum_1 id hw₂] at hw₃

Result:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : ∑ i ∈ t, w i • id i = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ x ∈ t, w x • x = x

Proof state:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : x ∈ ⋃ t, ⋃ (_ : ↑t ⊆ s), ⋃ (_ : AffineIndependent 𝕜 Subtype.val), (convexHull 𝕜) ↑t
⊢ ∃ ι x_1 z w,
    Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x

Tactic:
simp only [exists_prop, Set.mem_iUnion] at hx

Result:
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hx : ∃ i, ↑i ⊆ s ∧ AffineIndependent 𝕜 Subtype.val ∧ x ∈ (convexHull 𝕜) ↑i
⊢ ∃ ι x_1 z w,
    Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x

Proof state:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ i : { x // x ∈ t' }, (w ∘ Subtype.val) i • ↑i = x

Tactic:
change (∑ i ∈ t'.attach, (fun e => w e • e) ↑i) = x

Result:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ i ∈ t'.attach, (fun e => w e • e) ↑i = x

Proof state:
case intro.intro.intro.intro.intro.intro.refine_3
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∀ (i : { x // x ∈ t' }), 0 < (w ∘ Subtype.val) i

Tactic:
exact fun i =>
  (hw₁ _ (Finset.mem_filter.mp i.2).1).lt_of_ne (Finset.mem_filter.mp i.property).2.symm

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
ht₃ : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ ι x_1 z w,
    Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x

Tactic:
simp only [t.convexHull_eq, exists_prop, Set.mem_setOf_eq] at ht₃

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
ht₃ : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ ι x_1 z w,
    Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x

Proof state:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
e : E
a✝ : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
⊢ False

Tactic:
apply hwe

Result:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
e : E
a✝ : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
⊢ w e • e = 0

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
ht₃ : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ ι x_1 z w,
    Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x

Tactic:
obtain ⟨w, hw₁, hw₂, hw₃⟩ := ht₃

Result:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
⊢ ∃ ι x_1 z w,
    Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i : ι, w i = 1 ∧ ∑ i : ι, w i • z i = x

Proof state:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∀ x ∈ t, w x • x ≠ 0 → w x ≠ 0

Tactic:
intro e _ hwe contra

Result:
case intro.intro.intro.intro.intro.intro.refine_5
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
e : E
a✝ : e ∈ t
hwe : w e • e ≠ 0
contra : w e = 0
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.refine_4
𝕜 : Type u_1
E : Type u
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
t : Finset E
ht₁ : ↑t ⊆ s
ht₂ : AffineIndependent 𝕜 Subtype.val
w : E → 𝕜
hw₁ : ∀ y ∈ t, 0 ≤ w y
hw₂ : ∑ y ∈ t, w y = 1
hw₃ : t.centerMass w id = x
t' : Finset E := filter (fun i => w i ≠ 0) t
⊢ ∑ i : { x // x ∈ t' }, (w ∘ Subtype.val) i = 1

Tactic:
erw [Finset.sum_attach, Finset.sum_filter_ne_zero, hw₂]

Result:
no goals