-- Mathlib/Analysis/Convex/Radon.lean
theorem radon_partition {f : ι → E} (h : ¬ AffineIndependent 𝕜 f) :
    ∃ I, (convexHull 𝕜 (f '' I) ∩ convexHull 𝕜 (f '' Iᶜ)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := filter (fun i => 0 ≤ w i) s
J : Finset ι := filter (fun i => w i < 0) s
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
⊢ ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty

Tactic:
have hI : 0 < ∑ i ∈ I, w i := by
  rcases exists_pos_of_sum_zero_of_exists_nonzero _ h_wsum ⟨nonzero_w_index, h1, h2⟩
    with ⟨pos_w_index, h1', h2'⟩
  exact sum_pos' (fun _i hi ↦ (mem_filter.1 hi).2)
    ⟨pos_w_index, by simp only [I, mem_filter, h1', h2'.le, and_self, h2']⟩

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := filter (fun i => 0 ≤ w i) s
J : Finset ι := filter (fun i => w i < 0) s
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
hI : 0 < ∑ i ∈ I, w i
⊢ ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := filter (fun i => 0 ≤ w i) s
J : Finset ι := filter (fun i => w i < 0) s
p : E := I.centerMass w f
⊢ ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty

Tactic:
have hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0 := by
  simpa only [h_wsum, not_lt] using sum_filter_add_sum_filter_not s (fun i ↦ w i < 0) w

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := filter (fun i => 0 ≤ w i) s
J : Finset ι := filter (fun i => w i < 0) s
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
⊢ ∃ I, ((convexHull 𝕜) (f '' I) ∩ (convexHull 𝕜) (f '' Iᶜ)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := filter (fun i => 0 ≤ w i) s
J : Finset ι := filter (fun i => w i < 0) s
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
hI : 0 < ∑ i ∈ I, w i
hp : J.centerMass w f = p
⊢ J.centerMass w f ∈ (convexHull 𝕜) (f '' (↑I)ᶜ)

Tactic:
refine centerMass_mem_convexHull_of_nonpos _ (fun _ hi ↦ (mem_filter.mp hi).2.le) ?_
  (fun _i hi ↦ mem_image_of_mem _ fun hi' ↦ ?_)

Result:
case intro.intro.intro.intro.intro.intro.refine_2.refine_1
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := filter (fun i => 0 ≤ w i) s
J : Finset ι := filter (fun i => w i < 0) s
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
hI : 0 < ∑ i ∈ I, w i
hp : J.centerMass w f = p
⊢ ∑ i ∈ J, w i < 0

case intro.intro.intro.intro.intro.intro.refine_2.refine_2
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : ι → E
s : Finset ι
w : ι → 𝕜
h_wsum : s.sum w = 0
h_vsum : ∑ e ∈ s, w e • f e = 0
nonzero_w_index : ι
h1 : nonzero_w_index ∈ s
h2 : w nonzero_w_index ≠ 0
I : Finset ι := filter (fun i => 0 ≤ w i) s
J : Finset ι := filter (fun i => w i < 0) s
p : E := I.centerMass w f
hJI : ∑ j ∈ J, w j + ∑ i ∈ I, w i = 0
hI : 0 < ∑ i ∈ I, w i
hp : J.centerMass w f = p
_i : ι
hi : _i ∈ J
hi' : _i ∈ ↑I
⊢ False