-- Mathlib/Analysis/Convex/TotallyBounded.lean
theorem totallyBounded_convexHull (hs : TotallyBounded s) :
    TotallyBounded (convexHull ℝ s)

Proof state:
case right
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : (convexHull ℝ) t ⊆ ⋃ y ∈ t', y +ᵥ V
⊢ (convexHull ℝ) s ⊆ ⋃ y ∈ t', y +ᵥ U

Tactic:
simp only [iUnion_vadd_set, vadd_eq_add] at hts hts' ⊢

Result:
case right
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ) t ⊆ t' + V
⊢ (convexHull ℝ) s ⊆ t' + U

Proof state:
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
obtain ⟨W, hW₁, hW₂⟩ := exists_nhds_zero_half hU

Result:
case intro.intro
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
obtain ⟨t', ⟨htf', hts'⟩⟩ := (totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp
  (IsCompact.totallyBounded (Finite.isCompact_convexHull htf)) _ hV₁)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : (convexHull ℝ) t ⊆ ⋃ y ∈ t', y +ᵥ V
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Proof state:
case right
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ) t ⊆ t' + V
⊢ (convexHull ℝ) s ⊆ t' + U

Tactic:
calc convexHull ℝ s
  _ ⊆ convexHull ℝ (t + V) := convexHull_mono hts
  _ ⊆ convexHull ℝ t + convexHull ℝ V := convexHull_add_subset
  _ = convexHull ℝ t + V := by rw [hV₂.convexHull_eq]
  _ ⊆ t' + V + V := add_subset_add_right hts'
  _ = t' + (V + V) := by rw [add_assoc]
  _ ⊆ t' + (W + W) := add_subset_add_left (add_subset_add hV₃ hV₃)
  _ ⊆ t' + U := add_subset_add_left (add_subset_iff.mpr hW₂)

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
obtain ⟨V, ⟨hV₁, hV₂, hV₃⟩⟩ := (locallyConvexSpace_iff_exists_convex_subset_zero ℝ E).mp lcs W hW₁

Result:
case intro.intro.intro.intro.intro
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Proof state:
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded ((convexHull ℝ) s)

Tactic:
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]

Result:
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Proof state:
case intro.intro.intro.intro.intro
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
obtain ⟨t, ⟨htf, hts⟩⟩ := (totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp hs) _ hV₁

Result:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Proof state:
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ) t ⊆ t' + V
⊢ t' + V + V = t' + (V + V)

Tactic:
rw [add_assoc]

Result:
no goals