-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.convexHull_eq (s : Finset E) : convexHull R ↑s =
    { x : E | ∃ w : E → R, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x }

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
⊢ (convexHull R) ↑s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
refine Set.Subset.antisymm (convexHull_min ?_ ?_) ?_

Result:
case refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
⊢ ↑s ⊆ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

case refine_2
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
⊢ Convex R {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

case refine_3
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
⊢ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} ⊆ (convexHull R) ↑s

Proof state:
case refine_3
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
⊢ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} ⊆ (convexHull R) ↑s

Tactic:
rintro _ ⟨w, hw₀, hw₁, rfl⟩

Result:
case refine_3.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
w : E → R
hw₀ : ∀ y ∈ s, 0 ≤ w y
hw₁ : ∑ y ∈ s, w y = 1
⊢ s.centerMass w id ∈ (convexHull R) ↑s

Proof state:
case refine_1.refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
hx : x ∈ s
⊢ ∀ y ∈ s, 0 ≤ if x = y then 1 else 0

Tactic:
intros

Result:
case refine_1.refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
⊢ 0 ≤ if x = y✝ then 1 else 0

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : E
hi : i ∈ s
⊢ 0 ≤ a * wx i + b * wy i

Tactic:
apply_rules [add_nonneg, mul_nonneg, hwx₀, hwy₀]

Result:
no goals

Proof state:
case pos
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
h✝ : x = y✝
⊢ 0 ≤ 1

case neg
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
hx : x ∈ s
y✝ : E
a✝ : y✝ ∈ s
h✝ : ¬x = y✝
⊢ 0 ≤ 0

Tactic:
exacts [zero_le_one, le_refl 0]

Result:
no goals

Proof state:
case refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
hx : x ∈ ↑s
⊢ x ∈ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
rw [Finset.mem_coe] at hx

Result:
case refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
hx : x ∈ s
⊢ x ∈ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Proof state:
case refine_2
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
⊢ Convex R {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
rintro x ⟨wx, hwx₀, hwx₁, rfl⟩ y ⟨wy, hwy₀, hwy₁, rfl⟩ a b ha hb hab

Result:
case refine_2.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 : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • s.centerMass wx id + b • s.centerMass wy id ∈
    {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Proof state:
case refine_3.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
w : E → R
hw₀ : ∀ y ∈ s, 0 ≤ w y
hw₁ : ∑ y ∈ s, w y = 1
⊢ s.centerMass w id ∈ (convexHull R) ↑s

Tactic:
exact
  s.centerMass_mem_convexHull (fun x hx => hw₀ _ hx) (hw₁.symm ▸ zero_lt_one) fun x hx => hx

Result:
no goals

Proof state:
case refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
⊢ ↑s ⊆ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
intro x hx

Result:
case refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
hx : x ∈ ↑s
⊢ x ∈ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Proof state:
case refine_2.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 : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ s.centerMass (fun i => a * wx i + b * wy i) id ∈
    {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}

Tactic:
refine ⟨_, ?_, ?_, rfl⟩

Result:
case refine_2.intro.intro.intro.intro.intro.intro.refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∀ y ∈ s, 0 ≤ a * wx y + b * wy y

case refine_2.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ y ∈ s, (a * wx y + b * wy y) = 1

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
wx : E → R
hwx₀ : ∀ y ∈ s, 0 ≤ wx y
hwx₁ : ∑ y ∈ s, wx y = 1
wy : E → R
hwy₀ : ∀ y ∈ s, 0 ≤ wy y
hwy₁ : ∑ y ∈ s, wy y = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ y ∈ s, (a * wx y + b * wy y) = 1

Tactic:
simp only [Finset.sum_add_distrib, ← mul_sum, mul_one, *]

Result:
no goals

Proof state:
case refine_1.refine_2
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
x : E
hx : x ∈ s
⊢ (∑ y ∈ s, if x = y then 1 else 0) = 1

Tactic:
rw [Finset.sum_ite_eq, if_pos hx]

Result:
no goals