-- Mathlib/Analysis/Convex/Combination.lean
theorem AffineBasis.convexHull_eq_nonneg_coord {ι : Type*} (b : AffineBasis ι R E) :
    convexHull R (range b) = { x | ∀ i, 0 ≤ b.coord i x }

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
⊢ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x} = {x | ∀ (i : ι), 0 ≤ (b.coord i) x}

Tactic:
ext x

Result:
case h
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
x : E
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x} ↔
    x ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
⊢ x ∈ affineSpan R (Set.range ⇑b)

Tactic:
rw [b.tot]

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
x : E
hx : x ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
⊢ x ∈ ⊤

Proof state:
case h.refine_2.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
⊢ (affineCombination R s ⇑b) w ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x}

Tactic:
refine ⟨s, w, ?_, hw₁, rfl⟩

Result:
case h.refine_2.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
⊢ ∀ i ∈ s, 0 ≤ w i

Proof state:
case h.refine_2.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx : (affineCombination R s ⇑b) w ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
i : ι
hi : i ∈ s
⊢ 0 ≤ w i

Tactic:
specialize hx i

Result:
case h.refine_2.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₁ : ∑ i ∈ s, w i = 1
hx' : (affineCombination R s ⇑b) w ∈ affineSpan R (Set.range ⇑b)
i : ι
hi : i ∈ s
hx : 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)
⊢ 0 ≤ w i

Proof state:
case h.refine_1
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
x : E
⊢ x ∈ {x | ∃ s w, (∀ i ∈ s, 0 ≤ w i) ∧ s.sum w = 1 ∧ (affineCombination R s ⇑b) w = x} →
    x ∈ {x | ∀ (i : ι), 0 ≤ (b.coord i) x}

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

Result:
case h.refine_1.intro.intro.intro.intro
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
⊢ 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)