case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
⊢ Set.range v ⊆ {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}

case refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
⊢ Convex R {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}

case refine'_3
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
⊢ {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x} ⊆ ↑(convexHull R).toOrderHom (Set.range v)
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
⊢ ↑(convexHull R).toOrderHom (Set.range v) = {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
refine' Subset.antisymm (convexHull_min _ _) _
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
x : E
hx : x ∈ Set.range v
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
⊢ Set.range v ⊆ {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
intro x hx
case refine'_1.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
case refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
x : E
hx : x ∈ Set.range v
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
obtain ⟨i, hi⟩ := Set.mem_range.mp hx
no goals
case refine'_1.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
refine' ⟨{i}, Function.const ι (1 : R), by simp, by simp, by simp [hi]⟩
no goals
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ ∀ (i_1 : ι), i_1 ∈ {i} → 0 ≤ const ι 1 i_1
simp
no goals
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ Finset.sum {i} (const ι 1) = 1
simp
no goals
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i✝ j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
x : E
hx : x ∈ Set.range v
i : ι
hi : v i = x
⊢ ↑(affineCombination R {i} v) (const ι 1) = x
simp [hi]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • ↑(affineCombination R s v) w + b • ↑(affineCombination R s' v) w' ∈
    {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
case refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
⊢ Convex R {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
rintro x ⟨s, w, hw₀, hw₁, rfl⟩ y ⟨s', w', hw₀', hw₁', rfl⟩ a b ha hb hab
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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 x_1 x_2, ↑(affineCombination R s v) w = x}
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • ↑(affineCombination R s v) w + b • ↑(affineCombination R s' v) w' ∈
    {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
let W : ι → R := fun i => (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ a • ↑(affineCombination R s v) w + b • ↑(affineCombination R s' v) w' ∈
    {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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 x_1 x_2, ↑(affineCombination R s v) w = x}
have hW₁ : (s ∪ s').sum W = 1 := by
  rw [sum_add_distrib, ← sum_subset (subset_union_left s s'),
    ← sum_subset (subset_union_right s s'), sum_ite_of_true _ _ fun i hi => hi,
    sum_ite_of_true _ _ fun i hi => hi, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
    mul_one] <;> intro i _ hi' <;> simp [hi']
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∀ (i : ι), i ∈ s ∪ s' → 0 ≤ W i

case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ↑(affineCombination R (s ∪ s') v) W = a • ↑(affineCombination R s v) w + b • ↑(affineCombination R s' v) w'
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ a • ↑(affineCombination R s v) w + b • ↑(affineCombination R s' v) w' ∈
    {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x}
refine' ⟨s ∪ s', W, _, hW₁, _⟩
no goals
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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
⊢ Finset.sum (s ∪ s') W = 1
rw [sum_add_distrib, ← sum_subset (subset_union_left s s'),
  ← sum_subset (subset_union_right s s'), sum_ite_of_true _ _ fun i hi => hi,
  sum_ite_of_true _ _ fun i hi => hi, ← mul_sum, ← mul_sum, hw₁, hw₁', ← add_mul, hab,
  mul_one] <;> intro i _ hi' <;> simp [hi']
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i✝ j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
i : ι
⊢ 0 ≤ W i
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∀ (i : ι), i ∈ s ∪ s' → 0 ≤ W i
rintro i -
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i✝ j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
i : ι
⊢ 0 ≤ W i
by_cases hi : i ∈ s <;> by_cases hi' : i ∈ s' <;>
  simp [hi, hi', add_nonneg, mul_nonneg ha (hw₀ i _), mul_nonneg hb (hw₀' i _)]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∑ x in s ∪ s', (if x ∈ s then a * w x else 0) • v x + ∑ x in s ∪ s', (if x ∈ s' then b * w' x else 0) • v x =
    a • ∑ i in s, w i • v i + b • ∑ i in s', w' i • v i
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ↑(affineCombination R (s ∪ s') v) W = a • ↑(affineCombination R s v) w + b • ↑(affineCombination R s' v) w'
simp_rw [affineCombination_eq_linear_combination (s ∪ s') v _ hW₁,
  affineCombination_eq_linear_combination s v w hw₁,
  affineCombination_eq_linear_combination s' v w' hw₁', add_smul, sum_add_distrib]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∑ x in s, (if x ∈ s then a * w x else 0) • v x + ∑ x in s', (if x ∈ s' then b * w' x else 0) • v x =
    a • ∑ i in s, w i • v i + b • ∑ i in s', w' i • v i

case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∀ (x : ι), 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_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∀ (x : ι), x ∈ s ∪ s' → ¬x ∈ s → (if x ∈ s then a * w x else 0) • v x = 0
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∑ x in s ∪ s', (if x ∈ s then a * w x else 0) • v x + ∑ x in s ∪ s', (if x ∈ s' then b * w' x else 0) • v x =
    a • ∑ i in s, w i • v i + b • ∑ i in s', w' i • v i
rw [← sum_subset (subset_union_left s s'), ← sum_subset (subset_union_right s s')]
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∑ x in s, (if x ∈ s then a * w x else 0) • v x + ∑ x in s', (if x ∈ s' then b * w' x else 0) • v x =
    a • ∑ i in s, w i • v i + b • ∑ i in s', w' i • v i
simp only [ite_smul, sum_ite_of_true _ _ fun _ hi => hi, mul_smul, ← smul_sum]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i✝ j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
i : ι
a✝ : i ∈ s ∪ s'
hi' : ¬i ∈ s'
⊢ (if i ∈ s' then b * w' i else 0) • v i = 0
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∀ (x : ι), x ∈ s ∪ s' → ¬x ∈ s' → (if x ∈ s' then b * w' x else 0) • v x = 0
intro i _ hi'
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i✝ j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
i : ι
a✝ : i ∈ s ∪ s'
hi' : ¬i ∈ s'
⊢ (if i ∈ s' then b * w' i else 0) • v i = 0
simp [hi']
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i✝ j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
i : ι
a✝ : i ∈ s ∪ s'
hi' : ¬i ∈ s
⊢ (if i ∈ s then a * w i else 0) • v i = 0
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
⊢ ∀ (x : ι), x ∈ s ∪ s' → ¬x ∈ s → (if x ∈ s then a * w x else 0) • v x = 0
intro i _ hi'
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i✝ j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ (i : ι), i ∈ s' → 0 ≤ w' i
hw₁' : Finset.sum s' 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₁ : Finset.sum (s ∪ s') W = 1
i : ι
a✝ : i ∈ s ∪ s'
hi' : ¬i ∈ s
⊢ (if i ∈ s then a * w i else 0) • v i = 0
simp [hi']
case refine'_3.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ ↑(affineCombination R s v) w ∈ ↑(convexHull R).toOrderHom (Set.range v)
case refine'_3
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z v : ι → E
⊢ {x | ∃ s w x_1 x_2, ↑(affineCombination R s v) w = x} ⊆ ↑(convexHull R).toOrderHom (Set.range v)
rintro x ⟨s, w, hw₀, hw₁, rfl⟩
no goals
case refine'_3.intro.intro.intro.intro
R : Type u_2
E : Type u_1
F : Type ?u.160371
ι : Type u_3
ι' : Type ?u.160377
α : Type ?u.160380
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t : Finset ι
w✝ : ι → R
z v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
⊢ ↑(affineCombination R s v) w ∈ ↑(convexHull R).toOrderHom (Set.range v)
exact affineCombination_mem_convexHull hw₀ hw₁