R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
⊢ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x} = {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
⊢ ↑(convexHull R).toOrderHom (Set.range ↑b) = {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
rw [convexHull_range_eq_exists_affineCombination]
case h
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x} ↔ x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
⊢ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x} = {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
ext x
case h.refine'_1
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x} → x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}

case h.refine'_2
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x}
case h
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x} ↔ x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
refine' ⟨_, fun hx => _⟩
case h.refine'_1.intro.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
i : ι
⊢ 0 ≤ ↑(coord b i) (↑(affineCombination R s ↑b) w)
case h.refine'_1
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x} → x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
rintro ⟨s, w, hw₀, hw₁, rfl⟩ i
case pos
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ ↑(coord b i) (↑(affineCombination R s ↑b) w)

case neg
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
i : ι
hi : ¬i ∈ s
⊢ 0 ≤ ↑(coord b i) (↑(affineCombination R s ↑b) w)
case h.refine'_1.intro.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
i : ι
⊢ 0 ≤ ↑(coord b i) (↑(affineCombination R s ↑b) w)
by_cases hi : i ∈ s
case pos
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ w i
case pos
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ ↑(coord b i) (↑(affineCombination R s ↑b) w)
rw [b.coord_apply_combination_of_mem hi hw₁]
no goals
case pos
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ w i
exact hw₀ i hi
no goals
case neg
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw₁ : Finset.sum s w = 1
i : ι
hi : ¬i ∈ s
⊢ 0 ≤ ↑(coord b i) (↑(affineCombination R s ↑b) w)
rw [b.coord_apply_combination_of_not_mem hi hw₁]
case h.refine'_2
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
hx' : x ∈ affineSpan R (Set.range ↑b)
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x}
case h.refine'_2
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x}
have hx' : x ∈ affineSpan R (range b) := by
  rw [b.tot]
  exact AffineSubspace.mem_top R E x
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx : ↑(affineCombination R s ↑b) w ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
⊢ ↑(affineCombination R s ↑b) w ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x}
case h.refine'_2
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
hx' : x ∈ affineSpan R (Set.range ↑b)
⊢ x ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x}
obtain ⟨s, w, hw₁, rfl⟩ := (mem_affineSpan_iff_eq_affineCombination R E).mp hx'
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx : ↑(affineCombination R s ↑b) w ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx : ↑(affineCombination R s ↑b) w ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
⊢ ↑(affineCombination R s ↑b) w ∈ {x | ∃ s w x_1 x_2, ↑(affineCombination R s ↑b) w = x}
refine' ⟨s, w, _, hw₁, rfl⟩
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx : ↑(affineCombination R s ↑b) w ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
i : ι
hi : i ∈ s
⊢ 0 ≤ w i
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx : ↑(affineCombination R s ↑b) w ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i
intro i hi
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
i : ι
hi : i ∈ s
hx : 0 ≤ ↑(coord b i) (↑(affineCombination R s ↑b) w)
⊢ 0 ≤ w i
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx : ↑(affineCombination R s ↑b) w ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
i : ι
hi : i ∈ s
⊢ 0 ≤ w i
specialize hx i
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
i : ι
hi : i ∈ s
hx : 0 ≤ w i
⊢ 0 ≤ w i
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
i : ι
hi : i ∈ s
hx : 0 ≤ ↑(coord b i) (↑(affineCombination R s ↑b) w)
⊢ 0 ≤ w i
rw [b.coord_apply_combination_of_mem hi hw₁] at hx
no goals
case h.refine'_2.intro.intro.intro
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i in s, w i = 1
hx' : ↑(affineCombination R s ↑b) w ∈ affineSpan R (Set.range ↑b)
i : ι
hi : i ∈ s
hx : 0 ≤ w i
⊢ 0 ≤ w i
exact hx
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
⊢ x ∈ ⊤
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
⊢ x ∈ affineSpan R (Set.range ↑b)
rw [b.tot]
no goals
R : Type u_2
E : Type u_3
F : Type ?u.476113
ι✝ : Type ?u.476116
ι' : Type ?u.476119
α : Type ?u.476122
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 : ι✝ → E
inst✝ : Fintype ι✝
f : ι✝ → R
ι : Type u_1
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ ↑(coord b i) x}
⊢ x ∈ ⊤
exact AffineSubspace.mem_top R E x