awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
inl : ∀ (h : 𝓝[s \ {a}] a = ⊥), ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
inr : ∀ (has : (𝓝[s \ {a}] a).NeBot), ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x

Tactic:
rcases eq_or_neBot (𝓝[s \ {a}] a) with h | has

Premises used: nhdsWithin, SDiff.sdiff, Filter.eq_or_neBot, Singleton.singleton
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
inl : ∀ᶠ (x : 𝕜) in ⊥, s \ {a} ∈ 𝓝 x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
⊢ ∀ᶠ (x : 𝕜) in ⊥, s \ {a} ∈ 𝓝 x

Tactic:
eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
h : 𝓝[s \ {a}] a = ⊥
⊢ ∀ᶠ (x : 𝕜) in ⊥, s \ {a} ∈ 𝓝 x

Tactic:
exact eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : (𝓝[s \ {a}] a).NeBot
⊢ a ∈ closure[inst_3] s

Tactic:
replace has := closure_mono diff_subset (mem_closure_iff_nhdsWithin_neBot.2 has)
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
rw : 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a
| 𝓝[s \ {a}] a

Tactic:
rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left]

Premises used: Set.diff_eq, Set.Iio_union_Ioi, Set.inter_union_distrib_left
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
inr : ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x

Tactic:
conv in 𝓝[s \ {a}] a => rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left]

Premises used: Set.diff_eq, Set.Iio_union_Ioi, Set.inter_union_distrib_left
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
inr : (∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x) ∧ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a ∪ s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x

Tactic:
rw [nhdsWithin_union, eventually_sup]

Premises used: nhdsWithin_union, Filter.eventually_sup
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
⊢ (∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x) ∧ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x

Tactic:
⟨diff_singleton_eventually_mem_nhds_left fun x hx ↦ hs.Ioo_subset_of_mem_closure hx has,
    diff_singleton_eventually_mem_nhds_left (𝕜 := 𝕜ᵒᵈ) fun x hx z hz ↦
      hs.Ioo_subset_of_mem_closure has hx hz.symm⟩

Premises used: Convex.Ioo_subset_of_mem_closure, And.intro, _private.0.diff_singleton_eventually_mem_nhds_left, And.symm
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
⊢ (∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x) ∧ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Ioi a] a, s \ {a} ∈ 𝓝 x

Tactic:
exact ⟨diff_singleton_eventually_mem_nhds_left fun x hx ↦ hs.Ioo_subset_of_mem_closure hx has,
    diff_singleton_eventually_mem_nhds_left (𝕜 := 𝕜ᵒᵈ) fun x hx z hz ↦
      hs.Ioo_subset_of_mem_closure has hx hz.symm⟩
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
this :
  IsCompact.{u_5} (X := V)
    ((⇑(↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) : (a : P) → V) '' s.closedInterior)
apply :
  IsCompact.{u_5} (X := V) ((⇑(Homeomorph.symm (Homeomorph.vaddConst (s.points 0))) : (a : P) → V) '' s.closedInterior)
⊢ IsCompact s.closedInterior

Tactic:
apply (Homeomorph.vaddConst (s.points 0)).symm.isCompact_image.mp

Premises used: Affine.Simplex.points, Homeomorph.symm, Homeomorph.isCompact_image, Iff.mp, OfNat.ofNat, Homeomorph.vaddConst
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
this :
  IsCompact.{u_5} (X := V)
    ((⇑(↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) : (a : P) → V) '' s.closedInterior)
⊢ IsCompact.{u_5} (X := V) ((⇑(Homeomorph.symm (Homeomorph.vaddConst (s.points 0))) : (a : P) → V) '' s.closedInterior)

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
suffices :
  IsCompact.{u_5} (X := V)
    ((⇑(↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) : (a : P) → V) '' s.closedInterior)
⊢ IsCompact s.closedInterior

Tactic:
suffices IsCompact ((AffineEquiv.vaddConst 𝕜 (s.points 0)).symm.toAffineMap ''
      s.closedInterior) by
    apply (Homeomorph.vaddConst (s.points 0)).symm.isCompact_image.mp
    simpa
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
rw :
  IsCompact.{u_5} (X := V)
    ((convexHull 𝕜 : (a : Set V) → Set V)
      (range (s.map (↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) ⋯).points))
⊢ IsCompact.{u_5} (X := V)
    ((⇑(↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) : (a : P) → V) '' s.closedInterior)

Tactic:
rw [← s.closedInterior_map (AffineEquiv.injective _), ← convexHull_eq_closedInterior]

Premises used: Affine.Simplex.closedInterior_map, Affine.Simplex.convexHull_eq_closedInterior
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
⊢ IsCompact.{u_5} (X := V)
    ((convexHull 𝕜 : (a : Set V) → Set V)
      (range (s.map (↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) ⋯).points))

Tactic:
(Set.finite_range _).isCompact_convexHull 𝕜

Premises used: Set.Finite.isCompact_convexHull, Set.finite_range
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
n : ℕ
s : Simplex 𝕜 P n
⊢ IsCompact.{u_5} (X := V)
    ((convexHull 𝕜 : (a : Set V) → Set V)
      (range (s.map (↑(AffineEquiv.symm (AffineEquiv.vaddConst 𝕜 (s.points 0))) : P →ᵃ[𝕜] V) ⋯).points))

Tactic:
exact (Set.finite_range _).isCompact_convexHull 𝕜

Premises used: Set.Finite.isCompact_convexHull, Set.finite_range
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
V : Type u_5
P : Type u_6
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderClosedTopology 𝕜
inst_5 : CompactIccSpace 𝕜
inst_6 : ContinuousAdd 𝕜
inst_7 : AddCommGroup V
inst_8 : TopologicalSpace V
inst_9 : IsTopologicalAddGroup V
inst_10 : Module 𝕜 V
inst_11 : ContinuousSMul 𝕜 V
inst_12 : AffineSpace V P
inst_13 : TopologicalSpace P
inst_14 : IsTopologicalAddTorsor P
inst_15 : T2Space P
n : ℕ
s : Simplex 𝕜 P n
⊢ IsClosed s.closedInterior

Tactic:
s.isCompact_closedInterior.isClosed

Premises used: Affine.Simplex.isCompact_closedInterior, IsCompact.isClosed
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
rw :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (nhds 0) U →
      ∃ (t : Set E),
        t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
⊢ TotallyBounded.{u_1} (α := E) ((convexHull ℝ : (a : Set E) → Set E) s)

Tactic:
rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero]

Premises used: totallyBounded_iff_subset_finite_iUnion_nhds_zero
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
obtain :
  ∀ (W : Set E) (hW₁ : Membership.mem (γ := Filter E) (nhds 0) W) (hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U),
    ∃ (t : Set E),
      t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)

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

Premises used: exists_nhds_zero_half
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
obtain :
  ∀ (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (nhds 0) V) (hV₂ : Convex ℝ V) (hV₃ : V ⊆ W),
    ∃ (t : Set E),
      t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)

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

Premises used: Real, Iff.mp, locallyConvexSpace_iff_exists_convex_subset_zero
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
obtain :
  ∀ (t : Set E) (htf : t.Finite) (hts : s ⊆ ⋃ y ∈ t, y +ᵥ V),
    ∃ (t : Set E),
      t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)

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

Premises used: Iff.mp, totallyBounded_iff_subset_finite_iUnion_nhds_zero
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
obtain :
  ∀ (t' : Set E) (htf' : t'.Finite)
    (hts' : Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) (⋃ y ∈ t', y +ᵥ V : Set E)),
    ∃ (t : Set E),
      t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)

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

Premises used: Real, Set.Finite.isCompact_convexHull, IsCompact.totallyBounded, Iff.mp, totallyBounded_iff_subset_finite_iUnion_nhds_zero
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
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' : Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) (⋃ y ∈ t', y +ᵥ V : Set E)
right : Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t', y +ᵥ U : Set E)
⊢ ∃ (t : Set E),
    t.Finite ∧ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t, y +ᵥ U : Set E)

Tactic:
use t', htf'
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
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' : Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) (⋃ y ∈ t', y +ᵥ V : Set E)
right :
  ∀ (hts : s ⊆ t + V) (hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V),
    (convexHull ℝ : (a : Set E) → Set E) s ⊆ t' + U
⊢ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E) (⋃ y ∈ t', y +ᵥ U : Set E)

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

Premises used: vadd_eq_add, Set.iUnion_vadd_set
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V
⊢ Subset (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) s : Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (t + V) : Set E)

Tactic:
convexHull_mono hts

Premises used: convexHull_mono
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V
⊢ (convexHull ℝ : (a : Set E) → Set E) (t + V) ⊆
    HAdd.hAdd (α := Set E) (β := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E)
      ((convexHull ℝ : (a : Set E) → Set E) V : Set E)

Tactic:
convexHull_add_subset

Premises used: convexHull_add_subset
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V
rw rw₁ :
  HAdd.hAdd (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) V =
    HAdd.hAdd (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) V
⊢ HAdd.hAdd (α := Set E) (β := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E)
      ((convexHull ℝ : (a : Set E) → Set E) V : Set E) =
    HAdd.hAdd (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) V

Tactic:
rw [hV₂.convexHull_eq]

Premises used: Convex.convexHull_eq
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V
⊢ HAdd.hAdd (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) t : Set E) V ⊆ t' + V + V

Tactic:
add_subset_add_right hts'

Premises used: Set.add_subset_add_right
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V
rw rw₁ : t' + (V + V) = t' + (V + V)
⊢ t' + V + V = t' + (V + V)

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V
⊢ t' + (V + V) ⊆ t' + (W + W)

Tactic:
add_subset_add_left (add_subset_add hV₃ hV₃)

Premises used: Set.add_subset_add_left, Set.add_subset_add
-- Module: Mathlib.Analysis.Convex.TotallyBounded
Goal:
E : Type u_1
s : Set E
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : Membership.mem (γ := Filter E) (nhds 0) U
W : Set E
hW₁ : Membership.mem (γ := Filter E) (nhds 0) W
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : Membership.mem (γ := Filter E) (nhds 0) V
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ : (a : Set E) → Set E) t ⊆ t' + V
⊢ t' + (W + W) ⊆ t' + U

Tactic:
add_subset_add_left (add_subset_iff.mpr hW₂)

Premises used: Iff.mpr, Set.add_subset_add_left, Set.add_subset_iff