-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
lemma balancedHull_subset_convexHull_union_neg {s : Set E} :
    balancedHull ℝ s ⊆ convexHull ℝ (s ∪ -s)

Proof state:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2) • y + ((1 - r) / 2) • -y = (fun x => r • x) y

Tactic:
rw [smul_neg, ← sub_eq_add_neg, ← sub_smul]

Result:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2 - (1 - r) / 2) • y = (fun x => r • x) y

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ balancedHull ℝ s ⊆ (convexHull ℝ) (s ∪ -s)

Tactic:
intro a ha

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : E
ha : a ∈ balancedHull ℝ s
⊢ a ∈ (convexHull ℝ) (s ∪ -s)

Proof state:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this : 0 ≤ 1 + r
⊢ (fun x => r • x) y ∈ segment ℝ y (-y)

Tactic:
have : 0 ≤ 1 - r := sub_nonneg.2 (le_of_abs_le hr)

Result:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ (fun x => r • x) y ∈ segment ℝ y (-y)

Proof state:
case intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
⊢ (fun x => r • x) y ∈ (convexHull ℝ) (s ∪ -s)

Tactic:
apply segment_subset_convexHull (mem_union_left (-s) hy) (mem_union_right _ (neg_mem_neg.mpr hy))

Result:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
⊢ (fun x => r • x) y ∈ segment ℝ y (-y)

Proof state:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2 - (1 - r) / 2) • y = (fun x => r • x) y

Tactic:
apply congrFun (congrArg HSMul.hSMul _) y

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ (1 + r) / 2 - (1 - r) / 2 = r

Proof state:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
⊢ (fun x => r • x) y ∈ segment ℝ y (-y)

Tactic:
have : 0 ≤ 1 + r := neg_le_iff_add_nonneg'.mp (neg_le_of_abs_le hr)

Result:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this : 0 ≤ 1 + r
⊢ (fun x => r • x) y ∈ segment ℝ y (-y)

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ 0 ≤ (1 + r) / 2

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ (fun x => r • x) y ∈ segment ℝ y (-y)

Tactic:
refine ⟨(1 + r)/2, (1 - r)/2, by positivity, by positivity, by ring, ?_⟩

Result:
case intro.intro.intro.intro.a
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2) • y + ((1 - r) / 2) • -y = (fun x => r • x) y

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ 0 ≤ (1 - r) / 2

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ (1 + r) / 2 - (1 - r) / 2 = r

Tactic:
ring_nf

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
this✝ : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ (1 + r) / 2 + (1 - r) / 2 = 1

Tactic:
ring

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : E
ha : a ∈ balancedHull ℝ s
⊢ a ∈ (convexHull ℝ) (s ∪ -s)

Tactic:
obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 ha

Result:
case intro.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun x => r • x) y ∈ balancedHull ℝ s
⊢ (fun x => r • x) y ∈ (convexHull ℝ) (s ∪ -s)