awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
𝕜₁ :
  ∀ (s : Set E) (hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s),
    ∃ (i' : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s
⊢ Filter.HasBasis (𝓝 0) (fun (s : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) s ∧ AbsConvex 𝕜 s) id

Tactic:
refine
    (LocallyConvexSpace.convex_basis_zero 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs =>
      ⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩

Premises used: LocallyConvexSpace.convex_basis_zero, Eq.subset, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis, rfl
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
⊢ ∃ (i' : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s

Tactic:
⟨convexHull 𝕜 (balancedCore 𝕜 s), ?_, convexHull_min (balancedCore_subset s) hs.2⟩

Premises used: convexHull, And.right, And.intro, Exists.intro, balancedCore, convexHull_min, DFunLike.coe, balancedCore_subset
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
refine :
  Membership.mem (α := Set E) (γ := Filter E) (𝓝 0) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s) : Set E) ∧
    AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))
⊢ ∃ (i' : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s

Tactic:
refine ⟨convexHull 𝕜 (balancedCore 𝕜 s), ?_, convexHull_min (balancedCore_subset s) hs.2⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
⊢ Membership.mem (α := Set E) (γ := Filter E) (𝓝 0) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s) : Set E) ∧
    AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))

Tactic:
⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull 𝕜 _), ?_⟩

Premises used: subset_convexHull, balancedCore_mem_nhds_zero, And.left, And.intro, Filter.mem_of_superset
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
refine : AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))
⊢ Membership.mem (α := Set E) (γ := Filter E) (𝓝 0) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s) : Set E) ∧
    AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))

Tactic:
refine ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull 𝕜 _), ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
⊢ AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))

Tactic:
⟨(balancedCore_balanced s).convexHull, ?_⟩

Premises used: Balanced.convexHull, AbsConvex, And.intro, balancedCore_balanced
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
refine : Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))
⊢ AbsConvex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))

Tactic:
refine ⟨(balancedCore_balanced s).convexHull, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))

Tactic:
convex_convexHull 𝕜 (balancedCore 𝕜 s)

Premises used: convex_convexHull, balancedCore
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ Convex 𝕜 s
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ((convexHull 𝕜 : (a : Set E) → Set E) (balancedCore 𝕜 s))

Tactic:
exact convex_convexHull 𝕜 (balancedCore 𝕜 s)

Premises used: convex_convexHull, balancedCore
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
⊢ Filter.HasBasis (𝓝 0) (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_4] s ∧ AbsConvex 𝕜 s) id

Tactic:
(nhds_hasBasis_absConvex 𝕜 E).to_hasBasis ?_ ?_

Premises used: nhds_hasBasis_absConvex, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
refine_1 :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i ∧ AbsConvex 𝕜 i →
      ∃ (i' : Set E), (0 ∈ i' ∧ IsOpen[inst_4] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id i
refine_2 :
  ∀ (i' : Set E),
    0 ∈ i' ∧ IsOpen[inst_4] i' ∧ AbsConvex 𝕜 i' →
      ∃ (i : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id i'
⊢ Filter.HasBasis (𝓝 0) (fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_4] s ∧ AbsConvex 𝕜 s) id

Tactic:
refine (nhds_hasBasis_absConvex 𝕜 E).to_hasBasis ?_ ?_

Premises used: nhds_hasBasis_absConvex, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
s : Set E
hs_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex 𝕜 s
⊢ ∃ (i' : Set E), (0 ∈ i' ∧ IsOpen[inst_4] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s

Tactic:
⟨interior s, ?_, interior_subset⟩

Premises used: interior_subset, And.intro, interior, Exists.intro
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
s : Set E
hs_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex 𝕜 s
refine_1 : 0 ∈ interior s ∧ IsOpen[inst_4] (interior s) ∧ AbsConvex 𝕜 (interior s)
⊢ ∃ (i' : Set E), (0 ∈ i' ∧ IsOpen[inst_4] i' ∧ AbsConvex 𝕜 i') ∧ id i' ⊆ id s

Tactic:
refine ⟨interior s, ?_, interior_subset⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
s : Set E
hs_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex 𝕜 s
⊢ 0 ∈ interior s ∧ IsOpen[inst_4] (interior s) ∧ AbsConvex 𝕜 (interior s)

Tactic:
⟨mem_interior_iff_mem_nhds.mpr hs_nhds, isOpen_interior,
        hs_balanced.interior (mem_interior_iff_mem_nhds.mpr hs_nhds), hs_convex.interior⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, isOpen_interior, Balanced.interior, Convex.interior, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
s : Set E
hs_nhds : Membership.mem (γ := Filter E) (𝓝 0) s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex 𝕜 s
⊢ 0 ∈ interior s ∧ IsOpen[inst_4] (interior s) ∧ AbsConvex 𝕜 (interior s)

Tactic:
exact
      ⟨mem_interior_iff_mem_nhds.mpr hs_nhds, isOpen_interior,
        hs_balanced.interior (mem_interior_iff_mem_nhds.mpr hs_nhds), hs_convex.interior⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
s : Set E
hs_zero : 0 ∈ s
hs_open : IsOpen[inst_4] s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex 𝕜 s
⊢ ∃ (i : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s

Tactic:
⟨s, ⟨hs_open.mem_nhds hs_zero, hs_balanced, hs_convex⟩, rfl.subset⟩

Premises used: Eq.subset, And.intro, IsOpen.mem_nhds, Exists.intro, rfl
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : LocallyConvexSpace 𝕜 E
inst_6 : ContinuousSMul 𝕜 E
inst_7 : IsTopologicalAddGroup E
inst_8 : ZeroLEOneClass 𝕜
s : Set E
hs_zero : 0 ∈ s
hs_open : IsOpen[inst_4] s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex 𝕜 s
⊢ ∃ (i : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s

Tactic:
exact ⟨s, ⟨hs_open.mem_nhds hs_zero, hs_balanced, hs_convex⟩, rfl.subset⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s t : Set E
⊢ (absConvexHull 𝕜 : (a : Set E) → Set E) (s + t) ⊆
    HAdd.hAdd (α := Set E) (β := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)
      ((absConvexHull 𝕜 : (a : Set E) → Set E) t : Set E)

Tactic:
absConvexHull_min (add_subset_add subset_absConvexHull subset_absConvexHull)
    ⟨Balanced.add balanced_absConvexHull balanced_absConvexHull,
      Convex.add convex_absConvexHull convex_absConvexHull⟩

Premises used: subset_absConvexHull, Balanced.add, Convex.add, convex_absConvexHull, absConvexHull_min, Set.add_subset_add, And.intro, balanced_absConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ Eq (α := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E)
    ((convexHull 𝕜 : (a : Set E) → Set E) (balancedHull 𝕜 s) : Set E)

Tactic:
le_antisymm
  (absConvexHull_min
    ((subset_convexHull 𝕜 s).trans (convexHull_mono (subset_balancedHull 𝕜)))
      ⟨Balanced.convexHull (balancedHull.balanced s), convex_convexHull ..⟩)
  (convexHull_min (balanced_absConvexHull.balancedHull_subset_of_subset subset_absConvexHull)
      convex_absConvexHull)

Premises used: Balanced.convexHull, subset_absConvexHull, subset_convexHull, HasSubset.Subset.trans, subset_balancedHull, convex_convexHull, convexHull_mono, convex_absConvexHull, le_antisymm, Balanced.balancedHull_subset_of_subset, absConvexHull_min, And.intro, convexHull_min, balancedHull.balanced, balanced_absConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
⊢ Subset.{u_2} (α := Set E) (balancedHull 𝕜 ((convexHull 𝕜 : (a : Set E) → Set E) s))
    ((absConvexHull 𝕜 : (a : Set E) → Set E) s)

Tactic:
balanced_absConvexHull.balancedHull_subset_of_subset
    (convexHull_min subset_absConvexHull convex_absConvexHull)

Premises used: subset_absConvexHull, convex_absConvexHull, Balanced.balancedHull_subset_of_subset, convexHull_min, balanced_absConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
a : E
ha : a ∈ balancedHull ℝ s
obtain :
  ∀ (r : ℝ) (hr : ‖r‖ ≤ 1) (y : E) (hy : y ∈ s) (ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s),
    Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) ((fun (x : E) ↦ r • x) y)
⊢ Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) a

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

Premises used: mem_balancedHull_iff, Iff.mp, rfl
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
a : (fun (x : E) ↦ r • x) y ∈ segment ℝ y (-y)
⊢ Membership.mem (γ := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) ((fun (x : E) ↦ r • x) y)

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

Premises used: Iff.mpr, segment_subset_convexHull, Set.mem_union_right, Set.mem_union_left, Neg.neg, Set.neg_mem_neg
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
⊢ 0 ≤ 1 + r

Tactic:
have : 0 ≤ 1 + r := neg_le_iff_add_nonneg'.mp (neg_le_of_abs_le hr)
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
this : 0 ≤ 1 + r
⊢ 0 ≤ 1 - r

Tactic:
have : 0 ≤ 1 - r := sub_nonneg.2 (le_of_abs_le hr)
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
this_1 : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ 0 ≤ (1 + r) / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
this_1 : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ 0 ≤ (1 - r) / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
this_1 : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ (1 + r) / 2 + (1 - r) / 2 = 1

Tactic:
ring
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
this_1 : 0 ≤ 1 + r
this : 0 ≤ 1 - r
a : ((1 + r) / 2) • y + ((1 - r) / 2) • -y = (fun (x : E) ↦ r • x) y
⊢ (fun (x : E) ↦ r • x) y ∈ segment ℝ y (-y)

Tactic:
refine ⟨(1 + r)/2, (1 - r)/2, by positivity, by positivity, by ring, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
this_1 : 0 ≤ 1 + r
this : 0 ≤ 1 - r
a : ((1 + r) / 2 - (1 - r) / 2) • y = (fun (x : E) ↦ r • x) y
⊢ ((1 + r) / 2) • y + ((1 - r) / 2) • -y = (fun (x : E) ↦ r • x) y

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

Premises used: sub_eq_add_neg, sub_smul, smul_neg
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
r : ℝ
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
ha : (fun (x : E) ↦ r • x) y ∈ balancedHull ℝ s
this_1 : 0 ≤ 1 + r
this : 0 ≤ 1 - r
⊢ ((1 + r) / 2 - (1 - r) / 2) • y = (fun (x : E) ↦ r • x) y

Tactic:
ring_nf
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
rw :
  Eq (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (balancedHull ℝ s) : Set E)
⊢ Eq (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E)
    ((absConvexHull ℝ : (a : Set E) → Set E) s : Set E)

Tactic:
rw [absConvexHull_eq_convexHull_balancedHull]

Premises used: absConvexHull_eq_convexHull_balancedHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
h : x ∈ -s
rw : ∃ (r : ℝ), ‖r‖ ≤ 1 ∧ x ∈ r • s
⊢ x ∈ balancedHull ℝ s

Tactic:
rw [mem_balancedHull_iff]

Premises used: mem_balancedHull_iff
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
h_1 : x ∈ -s
h : norm (E := ℝ) (-1) ≤ 1 ∧ x ∈ HSMul.hSMul (α := ℝ) (-1) s
⊢ ∃ (r : ℝ), ‖r‖ ≤ 1 ∧ x ∈ r • s

Tactic:
use -1
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
h : x ∈ -s
⊢ norm (E := ℝ) (-1) ≤ 1 ∧ x ∈ HSMul.hSMul (α := ℝ) (-1) s

Tactic:
simp_all
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
rw :
  LE.le (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) (balancedHull ℝ s) : Set E)
    ((convexHull ℝ : (a : Set E) → Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) : Set E)
⊢ LE.le (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) (balancedHull ℝ s) : Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E)

Tactic:
rw [← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))]

Premises used: Real, convex_convexHull, Convex.convexHull_eq, Union.union, Neg.neg
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
⊢ LE.le (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) (balancedHull ℝ s) : Set E)
    ((convexHull ℝ : (a : Set E) → Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) : Set E)

Tactic:
convexHull_mono balancedHull_subset_convexHull_union_neg

Premises used: balancedHull_subset_convexHull_union_neg, convexHull_mono
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
⊢ LE.le (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) (balancedHull ℝ s) : Set E)
    ((convexHull ℝ : (a : Set E) → Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E) : Set E)

Tactic:
exact convexHull_mono balancedHull_subset_convexHull_union_neg

Premises used: balancedHull_subset_convexHull_union_neg, convexHull_mono
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
⊢ Eq (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E)
    ((convexHull ℝ : (a : Set E) → Set E) (balancedHull ℝ s) : Set E)

Tactic:
exact le_antisymm (convexHull_mono (union_subset (subset_balancedHull ℝ)
    (fun _ _ => by rw [mem_balancedHull_iff]; use -1; simp_all)))
    (by
      rw [← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))]
      exact convexHull_mono balancedHull_subset_convexHull_union_neg)

Premises used: Real, subset_balancedHull, convexHull_mono, Set.union_subset, le_antisymm
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
rw : TotallyBounded.{u_2} (α := E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s))
⊢ TotallyBounded.{u_2} (α := E) ((absConvexHull ℝ : (a : Set E) → Set E) s)

Tactic:
rw [← convexHull_union_neg_eq_absConvexHull]

Premises used: convexHull_union_neg_eq_absConvexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
hs₁ : TotallyBounded (s ∪ -s)
⊢ TotallyBounded.{u_2} (α := E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s))

Tactic:
apply totallyBounded_convexHull

Premises used: totallyBounded_convexHull
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
hs₁ : TotallyBounded s ∧ TotallyBounded (-s)
⊢ TotallyBounded (s ∪ -s)

Tactic:
rw [totallyBounded_union]

Premises used: totallyBounded_union
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded s ∧ TotallyBounded (-s)

Tactic:
⟨hs, totallyBounded_neg hs⟩

Premises used: totallyBounded_neg, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst_4 : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ TotallyBounded s ∧ TotallyBounded (-s)

Tactic:
exact ⟨hs, totallyBounded_neg hs⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
𝕜 : Type u_1
E : Type u_2
s : Set E
inst : SeminormedRing 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : Nonempty.{u_2 + 1} (↑s : Type u_2)
⊢ Membership.mem (γ := Set E) ((absConvexHull 𝕜 : (a : Set E) → Set E) s : Set E) 0

Tactic:
balanced_absConvexHull.zero_mem (Nonempty.mono subset_absConvexHull Set.Nonempty.of_subtype)

Premises used: Set.Nonempty.of_subtype, subset_absConvexHull, Set.Nonempty.mono, balanced_absConvexHull, Balanced.zero_mem
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : QuasiCompleteSpace ℝ E
s : Set E
ht : TotallyBounded s
rw : IsCompact.{u_3} (X := E) (closure[inst_2.toTopologicalSpace] ((absConvexHull ℝ : (a : Set E) → Set E) s))
⊢ IsCompact.{u_3} (X := E) ((closedAbsConvexHull ℝ : (a : Set E) → Set E) s)

Tactic:
rw [closedAbsConvexHull_eq_closure_absConvexHull]

Premises used: closedAbsConvexHull_eq_closure_absConvexHull