-- Mathlib/Analysis/Convex/Combination.lean
/-- The convex hull of `s` is equal to the set of centers of masses of finite families of points in
`s`.

For universe reasons, you shouldn't use this lemma to prove that a given center of mass belongs
to the convex hull. Use `mem_convexHull_of_exists_fintype` of the convex hull instead. -/
lemma mem_convexHull_iff_exists_fintype {s : Set E} {x : E} :
    x ∈ convexHull R s ↔ ∃ (ι : Type) (_ : Fintype ι) (w : ι → R) (z : ι → E), (∀ i, 0 ≤ w i) ∧
      ∑ i, w i = 1 ∧ (∀ i, z i ∈ s) ∧ ∑ i, w i • z i = x

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
h : (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x
⊢ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Tactic:
refine ⟨t, inferInstance, w ∘ (↑), z ∘ (↑), ?_⟩

Result:
case mp.intro.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
h : (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x
⊢ (∀ (i : { x // x ∈ t }), 0 ≤ (w ∘ Subtype.val) i) ∧
    ∑ i : { x // x ∈ t }, (w ∘ Subtype.val) i = 1 ∧
      (∀ (i : { x // x ∈ t }), (z ∘ Subtype.val) i ∈ s) ∧
        ∑ i : { x // x ∈ t }, (w ∘ Subtype.val) i • (z ∘ Subtype.val) i = x

Proof state:
case mp
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
⊢ x ∈ (convexHull R) s →
    ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Tactic:
simp only [convexHull_eq, mem_setOf_eq]

Result:
case mp
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
⊢ (∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x) →
    ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
⊢ x ∈ (convexHull R) s ↔
    ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Tactic:
constructor

Result:
case mp
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
⊢ x ∈ (convexHull R) s →
    ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

case mpr
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
⊢ (∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x) →
    x ∈ (convexHull R) s

Proof state:
case mpr
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
⊢ (∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x) →
    x ∈ (convexHull R) s

Tactic:
rintro ⟨ι, _, w, z, hw₀, hw₁, hz, hx⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
ι : Type
w✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ x ∈ (convexHull R) s

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
ι : Type
w✝ : Fintype ι
w : ι → R
z : ι → E
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
hz : ∀ (i : ι), z i ∈ s
hx : ∑ i : ι, w i • z i = x
⊢ x ∈ (convexHull R) s

Tactic:
exact mem_convexHull_of_exists_fintype w z hw₀ hw₁ hz hx

Result:
no goals

Proof state:
case mp
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
⊢ (∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x) →
    ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Tactic:
rintro ⟨ι, t, w, z, h⟩

Result:
case mp.intro.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
h : (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x
⊢ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i : ι, w i • z i = x

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
x : E
ι : Type
t : Finset ι
w : ι → R
z : ι → E
h : (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x
⊢ (∀ (i : { x // x ∈ t }), 0 ≤ (w ∘ Subtype.val) i) ∧
    ∑ i : { x // x ∈ t }, (w ∘ Subtype.val) i = 1 ∧
      (∀ (i : { x // x ∈ t }), (z ∘ Subtype.val) i ∈ s) ∧
        ∑ i : { x // x ∈ t }, (w ∘ Subtype.val) i • (z ∘ Subtype.val) i = x

Tactic:
simpa [← sum_attach t, centerMass_eq_of_sum_1 _ _ h.2.1] using h

Result:
no goals