-- Mathlib/Analysis/Convex/Combination.lean
theorem convexHull_range_eq_exists_affineCombination (v : ι → E) : convexHull R (range v) =
    { x | ∃ (s : Finset ι) (w : ι → R), (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧
      s.affineCombination R v w = x }

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ (s ∪ s').sum W = 1

Tactic:
rw [sum_add_distrib, ← sum_subset subset_union_left,
  ← sum_subset subset_union_right, sum_ite_of_true,
  sum_ite_of_true, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
  mul_one] <;> intros <;> simp_all

Result:
no goals

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ ∑ x ∈ s ∪ s', (if x ∈ s then a * w x else 0) • v x + ∑ x ∈ s ∪ s', (if x ∈ s' then b * w' x else 0) • v x =
    a • ∑ i ∈ s, w i • v i + b • ∑ i ∈ s', w' i • v i

Tactic:
rw [← sum_subset subset_union_left, ← sum_subset subset_union_right]

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ ∑ x ∈ s, (if x ∈ s then a * w x else 0) • v x + ∑ x ∈ s', (if x ∈ s' then b * w' x else 0) • v x =
    a • ∑ i ∈ s, w i • v i + b • ∑ i ∈ s', w' i • v i

case refine_2.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ ∀ x ∈ s ∪ s', x ∉ s' → (if x ∈ s' then b * w' x else 0) • v x = 0

case refine_2.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ ∀ x ∈ s ∪ s', x ∉ s → (if x ∈ s then a * w x else 0) • v x = 0

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
⊢ 0 ≤ W i

Tactic:
by_cases hi : i ∈ s <;> by_cases hi' : i ∈ s' <;>
  simp [W, hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]

Result:
no goals

Proof state:
case refine_1
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
⊢ Set.range v ⊆ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Tactic:
intro x hx

Result:
case refine_1
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
x : E
hx : x ∈ Set.range v
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
⊢ a • (affineCombination R s v) w + b • (affineCombination R s' v) w' ∈
    {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Tactic:
have hW₁ : (s ∪ s').sum W = 1 := by
  rw [sum_add_distrib, ← sum_subset subset_union_left,
    ← sum_subset subset_union_right, sum_ite_of_true,
    sum_ite_of_true, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
    mul_one] <;> intros <;> simp_all

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
⊢ a • (affineCombination R s v) w + b • (affineCombination R s' v) w' ∈
    {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ (affineCombination R {i} v) (const ι 1) = x

Tactic:
simp [hi]

Result:
no goals

Proof state:
case refine_3
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
⊢ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x} ⊆ (convexHull R) (Set.range v)

Tactic:
rintro x ⟨s, w, hw₀, hw₁, rfl⟩

Result:
case refine_3.intro.intro.intro.intro
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
⊢ (affineCombination R s v) w ∈ (convexHull R) (Set.range v)

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ ∀ i_1 ∈ {i}, 0 ≤ const ι 1 i_1

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
x : E
hx : x ∈ Set.range v
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}

Tactic:
obtain ⟨i, hi⟩ := Set.mem_range.mp hx

Result:
case refine_1.intro
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s v) w = x}