awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t
rcases : ∀ (t : Set E) (ht1 : Balanced 𝕜 t) (ht2 : t ⊆ s) (hy : y ∈ t), (fun (x : E) ↦ a • x) y ∈ balancedCore 𝕜 s
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCore 𝕜 s

Tactic:
rcases hy with ⟨t, ht1, ht2, hy⟩
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
t : Set E
ht1 : Balanced 𝕜 t
ht2 : t ⊆ s
hy : y ∈ t
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCore 𝕜 s

Tactic:
⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩

Premises used: Set.Mem, setOf, Set.sUnion, And.intro, Exists.intro, balancedCore, Set.smul_mem_smul_set
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
t : Set E
ht1 : Balanced 𝕜 t
ht2 : t ⊆ s
hy : y ∈ t
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCore 𝕜 s

Tactic:
exact ⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
⊢ Balanced 𝕜 (balancedCore 𝕜 s)

Tactic:
fun _ =>
  smul_balancedCore_subset s

Premises used: smul_balancedCore_subset, Balanced
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
hs : Balanced 𝕜 s
h : s ⊆ t
⊢ s ⊆ balancedCore 𝕜 t

Tactic:
subset_sUnion_of_mem ⟨hs, h⟩

Premises used: And.intro, balancedCore, Set.subset_sUnion_of_mem
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
h : Balanced 𝕜 s
⊢ balancedCore 𝕜 s = s

Tactic:
le_antisymm (balancedCore_subset _) (h.subset_balancedCore_of_subset subset_rfl)

Premises used: le_antisymm, subset_rfl, balancedCore_subset, Balanced.subset_balancedCore_of_subset
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
x : E
⊢ x ∈ balancedCoreAux 𝕜 s ↔ ∀ (r : 𝕜), 1 ≤ ‖r‖ → x ∈ r • s

Tactic:
mem_iInter₂

Premises used: Set.Mem, Set.mem_iInter₂, balancedCoreAux
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
x : E
⊢ x ∈ balancedHull 𝕜 s ↔ ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • s

Tactic:
simp [balancedHull]

Premises used: balancedHull
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
obtain :
  ∀ (r : 𝕜) (hr : ‖r‖ ≤ 1) (y : E) (hy : y ∈ s) (hx : (fun (x : E) ↦ r • x) y ∈ balancedHull 𝕜 s),
    (fun (x : E) ↦ r • x) y ∈ t
⊢ x ∈ t

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

Premises used: mem_balancedHull_iff, Iff.mp, rfl
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
r : 𝕜
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
hx : (fun (x : E) ↦ r • x) y ∈ balancedHull 𝕜 s
⊢ (fun (x : E) ↦ r • x) y ∈ t

Tactic:
ht.smul_mem hr (h hy)

Premises used: Set.Mem, Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
r : 𝕜
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
hx : (fun (x : E) ↦ r • x) y ∈ balancedHull 𝕜 s
⊢ (fun (x : E) ↦ r • x) y ∈ t

Tactic:
exact ht.smul_mem hr (h hy)

Premises used: Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
rw : ∀ (hx : ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • s), ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • t
⊢ x ∈ balancedHull 𝕜 t

Tactic:
rw [mem_balancedHull_iff] at *

Premises used: mem_balancedHull_iff
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
hx : ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • s
obtain : ∀ (r : 𝕜) (hr₁ : ‖r‖ ≤ 1) (hr₂ : x ∈ r • s), ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • t
⊢ ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • t

Tactic:
obtain ⟨r, hr₁, hr₂⟩ := hx
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
r : 𝕜
hr₁ : ‖r‖ ≤ 1
hr₂ : x ∈ r • s
h : ‖r‖ ≤ 1 ∧ x ∈ r • t
⊢ ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • t

Tactic:
use r
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
r : 𝕜
hr₁ : ‖r‖ ≤ 1
hr₂ : x ∈ r • s
⊢ ‖r‖ ≤ 1 ∧ x ∈ r • t

Tactic:
⟨hr₁, smul_set_mono hst hr₂⟩

Premises used: Set.smul_set_mono, And.intro
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
r : 𝕜
hr₁ : ‖r‖ ≤ 1
hr₂ : x ∈ r • s
⊢ ‖r‖ ≤ 1 ∧ x ∈ r • t

Tactic:
exact ⟨hr₁, smul_set_mono hst hr₂⟩
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ 0 ∈ balancedCore 𝕜 s

Tactic:
mem_balancedCore_iff.2 ⟨0, balanced_zero, zero_subset.2 hs, Set.zero_mem_zero⟩

Premises used: Iff.mpr, Set.zero_mem_zero, Set.zero_subset, And.intro, Exists.intro, OfNat.ofNat, mem_balancedCore_iff, balanced_zero
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
⊢ (balancedCore 𝕜 s).Nonempty ↔ 0 ∈ s

Tactic:
⟨fun h => zero_subset.1 <| (zero_smul_set h).superset.trans <|
    (balancedCore_balanced s (0 : 𝕜) <| norm_zero.trans_le zero_le_one).trans <|
      balancedCore_subset _,
    fun h => ⟨0, balancedCore_zero_mem h⟩⟩

Premises used: norm_zero, HasSubset.Subset.trans, Eq.trans_le, Set.zero_smul_set, zero_le_one, Set.zero_subset, Iff.intro, Exists.intro, Iff.mp, balancedCore_balanced, balancedCore_zero_mem, OfNat.ofNat, Eq.superset, balancedCore_subset
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : Balanced 𝕜 s
hs_nonempty : s.Nonempty
⊢ (balancedCore 𝕜 s).Nonempty

Tactic:
rw [← hs.balancedCore_eq] at hs_nonempty

Premises used: Balanced.balancedCore_eq
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : Balanced 𝕜 s
hs_nonempty : (balancedCore 𝕜 s).Nonempty
⊢ 0 ∈ s

Tactic:
balancedCore_nonempty_iff.mp hs_nonempty

Premises used: balancedCore_nonempty_iff, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : Balanced 𝕜 s
hs_nonempty : (balancedCore 𝕜 s).Nonempty
⊢ 0 ∈ s

Tactic:
exact balancedCore_nonempty_iff.mp hs_nonempty

Premises used: balancedCore_nonempty_iff, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormOneClass 𝕜
s : Set E
⊢ s ⊆ balancedHull 𝕜 s

Tactic:
fun _ hx =>
  mem_balancedHull_iff.2 ⟨1, norm_one.le, _, hx, one_smul _ _⟩

Premises used: Iff.mpr, NormOneClass.norm_one, Eq.le, mem_balancedHull_iff, Set.Subset, one_smul, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
simp_rw : ∀ (x : E), (∃ (i : 𝕜) (_ : ‖i‖ ≤ 1), x ∈ a • i • s) → ∃ (i : 𝕜) (_ : ‖i‖ ≤ 1), x ∈ i • s
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s

Tactic:
simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]

Premises used: Set.smul_set_iUnion₂, Set.subset_def, Set.mem_iUnion₂, balancedHull
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ a • r • s
⊢ x ∈ (a • r) • s

Tactic:
rw [← smul_assoc] at hx

Premises used: smul_assoc
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ (a • r) • s
⊢ ∃ (i : 𝕜) (_ : ‖i‖ ≤ 1), x ∈ i • s

Tactic:
⟨a • r, (norm_mul_le _ _).trans (mul_le_one₀ ha (norm_nonneg r) hr), hx⟩

Premises used: mul_le_one₀, Exists.intro, HSMul.hSMul, LE.le.trans, norm_mul_le, norm_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ (a • r) • s
⊢ ∃ (i : 𝕜) (_ : ‖i‖ ≤ 1), x ∈ i • s

Tactic:
exact ⟨a • r, (norm_mul_le _ _).trans (mul_le_one₀ ha (norm_nonneg r) hr), hx⟩
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
inst_3 : NormOneClass 𝕜
t : Set E
⊢ balancedHull 𝕜 (s + t) ⊆ balancedHull 𝕜 s + balancedHull 𝕜 t

Tactic:
balancedHull_subset_of_subset (add (balancedHull.balanced _) (balancedHull.balanced _))
    (add_subset_add (subset_balancedHull _) (subset_balancedHull _))

Premises used: Balanced.add, subset_balancedHull, Balanced.balancedHull_subset_of_subset, Set.add_subset_add, balancedHull.balanced
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
simp_rw : ∀ (a : E), ∃ (i : 𝕜) (_ : 1 ≤ ‖i‖), a ∉ ∅
⊢ Eq.{u_2 + 1} (α := Set E) (balancedCoreAux 𝕜 ∅) ∅

Tactic:
simp_rw [balancedCoreAux, iInter₂_eq_empty_iff, smul_set_empty]

Premises used: Set.smul_set_empty, balancedCoreAux, Set.iInter₂_eq_empty_iff
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
⊢ ∀ (a : E), ∃ (i : 𝕜) (_ : 1 ≤ ‖i‖), a ∉ ∅

Tactic:
fun _ => ⟨1, norm_one.ge, notMem_empty _⟩

Premises used: Eq.ge, NormOneClass.norm_one, Exists.intro, Set.notMem_empty, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
⊢ ∀ (a : E), ∃ (i : 𝕜) (_ : 1 ≤ ‖i‖), a ∉ ∅

Tactic:
exact fun _ => ⟨1, norm_one.ge, notMem_empty _⟩
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
x : E
hx : x ∈ balancedCoreAux 𝕜 s
⊢ x ∈ s

Tactic:
simpa only [one_smul] using mem_balancedCoreAux_iff.1 hx 1 norm_one.ge

Premises used: Eq.ge, mem_balancedCoreAux_iff, NormOneClass.norm_one, one_smul, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCoreAux 𝕜 s
inl :
  ∀ (ha : norm.{u_1} (E := 𝕜) 0 ≤ 1), (fun (x : E) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) y ∈ balancedCoreAux 𝕜 s
inr : ∀ (h : a ≠ 0), (fun (x : E) ↦ a • x) y ∈ balancedCoreAux 𝕜 s
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCoreAux 𝕜 s

Tactic:
obtain rfl | h := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
y : E
hy : y ∈ balancedCoreAux 𝕜 s
ha : norm.{u_1} (E := 𝕜) 0 ≤ 1
inl inl₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ balancedCoreAux 𝕜 s
inl₂ : 0 ∈ balancedCoreAux 𝕜 s
⊢ (fun (x : E) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) y ∈ balancedCoreAux 𝕜 s

Tactic:
simp_rw [zero_smul, h0]

Premises used: zero_smul
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCoreAux 𝕜 s
h : a ≠ 0
inr : ∀ (hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s) (h : a ≠ 0) (r : 𝕜), 1 ≤ ‖r‖ → (fun (x : E) ↦ a • x) y ∈ r • s
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCoreAux 𝕜 s

Tactic:
rw [mem_balancedCoreAux_iff] at hy ⊢

Premises used: mem_balancedCoreAux_iff
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
rw : 1 ≤ ‖a‖⁻¹ * ‖r‖
⊢ 1 ≤ ‖a⁻¹ • r‖

Tactic:
rw [norm_smul, norm_inv]

Premises used: norm_smul, norm_inv
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a‖⁻¹ * ‖r‖

Tactic:
one_le_mul_of_one_le_of_one_le ((one_le_inv₀ (norm_pos_iff.mpr h)).2 ha) hr

Premises used: Iff.mpr, norm_pos_iff, one_le_inv₀, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a‖⁻¹ * ‖r‖

Tactic:
exact one_le_mul_of_one_le_of_one_le ((one_le_inv₀ (norm_pos_iff.mpr h)).2 ha) hr

Premises used: Iff.mpr, norm_pos_iff, one_le_inv₀, one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a⁻¹ • r‖

Tactic:
have h'' : 1 ≤ ‖a⁻¹ • r‖ := by
    rw [norm_smul, norm_inv]
    exact one_le_mul_of_one_le_of_one_le ((one_le_inv₀ (norm_pos_iff.mpr h)).2 ha) hr
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
h'' : 1 ≤ ‖a⁻¹ • r‖
⊢ y ∈ (a⁻¹ • r) • s

Tactic:
have h' := hy (a⁻¹ • r) h''
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
h'' : 1 ≤ ‖a⁻¹ • r‖
h' : y ∈ (a⁻¹ • r) • s
inr : ∀ (h' : y ∈ a⁻¹ • r • s), (fun (x : E) ↦ a • x) y ∈ r • s
inr₁ inr₂ inr₃ inr₄ : ∀ (h' : a • y ∈ r • s), (fun (x : E) ↦ a • x) y ∈ r • s
⊢ (fun (x : E) ↦ a • x) y ∈ r • s

Tactic:
rwa [smul_assoc, mem_inv_smul_set_iff₀ h] at h'

Premises used: Set.mem_inv_smul_set_iff₀, smul_assoc
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
⊢ t ⊆ balancedCoreAux 𝕜 s

Tactic:
fun x hx => mem_balancedCoreAux_iff.2 fun r hr => ?_

Premises used: Iff.mpr, mem_balancedCoreAux_iff, Set.Subset
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
refine : ∀ (x : E) (hx : x ∈ t) (r : 𝕜) (hr : 1 ≤ ‖r‖), x ∈ r • s
⊢ t ⊆ balancedCoreAux 𝕜 s

Tactic:
refine fun x hx => mem_balancedCoreAux_iff.2 fun r hr => ?_

Premises used: Iff.mpr, mem_balancedCoreAux_iff
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
rw : r⁻¹ • x ∈ s
⊢ x ∈ r • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp <| zero_lt_one.trans_le hr)]

Premises used: norm_pos_iff, zero_lt_one, LT.lt.trans_le, Iff.mp, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ r⁻¹ • x ∈ s

Tactic:
h (ht.smul_mem ?_ hx)

Premises used: Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
refine : ‖r⁻¹‖ ≤ 1
⊢ r⁻¹ • x ∈ s

Tactic:
refine h (ht.smul_mem ?_ hx)

Premises used: Balanced.smul_mem
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
rw : ‖r‖⁻¹ ≤ 1
⊢ ‖r⁻¹‖ ≤ 1

Tactic:
rw [norm_inv]

Premises used: norm_inv
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r‖⁻¹ ≤ 1

Tactic:
inv_le_one_of_one_le₀ hr

Premises used: inv_le_one_of_one_le₀
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r‖⁻¹ ≤ 1

Tactic:
exact inv_le_one_of_one_le₀ hr

Premises used: inv_le_one_of_one_le₀
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
⊢ balancedCore 𝕜 s ⊆ balancedCoreAux 𝕜 s

Tactic:
balancedCoreAux_maximal (balancedCore_subset s) (balancedCore_balanced s)

Premises used: balancedCoreAux_maximal, balancedCore_balanced, balancedCore_subset
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ balancedCore 𝕜 s = ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • s

Tactic:
balancedCore_subset_balancedCoreAux.antisymm ?_

Premises used: HasSubset.Subset.antisymm, balancedCoreAux, balancedCore_subset_balancedCoreAux
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : 0 ∈ s
refine : balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s
⊢ balancedCore 𝕜 s = ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • s

Tactic:
refine balancedCore_subset_balancedCoreAux.antisymm ?_

Premises used: HasSubset.Subset.antisymm, balancedCore_subset_balancedCoreAux
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s

Tactic:
(balancedCoreAux_balanced ?_).subset_balancedCore_of_subset (balancedCoreAux_subset s)

Premises used: balancedCoreAux_balanced, balancedCoreAux_subset, Balanced.subset_balancedCore_of_subset
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : 0 ∈ s
refine : 0 ∈ balancedCoreAux 𝕜 s
⊢ balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s

Tactic:
refine (balancedCoreAux_balanced ?_).subset_balancedCore_of_subset (balancedCoreAux_subset s)

Premises used: balancedCoreAux_balanced, balancedCoreAux_subset, Balanced.subset_balancedCore_of_subset
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ 0 ∈ balancedCoreAux 𝕜 s

Tactic:
balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)

Premises used: balancedCore_zero_mem, balancedCore_subset_balancedCoreAux
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s : Set E
hs : 0 ∈ s
⊢ 0 ∈ balancedCoreAux 𝕜 s

Tactic:
exact balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)

Premises used: balancedCore_zero_mem, balancedCore_subset_balancedCoreAux
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
rw : s ⊆ ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • t
⊢ s ⊆ balancedCore 𝕜 t

Tactic:
rw [balancedCore_eq_iInter ht]

Premises used: balancedCore_eq_iInter
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • t

Tactic:
subset_iInter₂ fun a ha ↦ ?_

Premises used: Set.subset_iInter₂
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
refine : ∀ (a : 𝕜) (ha : 1 ≤ ‖a‖), s ⊆ a • t
⊢ s ⊆ ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • t

Tactic:
refine subset_iInter₂ fun a ha ↦ ?_

Premises used: Set.subset_iInter₂
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
rw : a⁻¹ • s ⊆ t
⊢ s ⊆ a • t

Tactic:
rw [subset_smul_set_iff₀ (norm_pos_iff.mp <| zero_lt_one.trans_le ha)]

Premises used: norm_pos_iff, zero_lt_one, LT.lt.trans_le, Iff.mp, Set.subset_smul_set_iff₀
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
a₁ : ‖a⁻¹‖ ≤ 1
⊢ a⁻¹ • s ⊆ t

Tactic:
apply hst
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
a₁ : ‖a‖⁻¹ ≤ 1
⊢ ‖a⁻¹‖ ≤ 1

Tactic:
rw [norm_inv]

Premises used: norm_inv
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1

Tactic:
inv_le_one_of_one_le₀ ha

Premises used: inv_le_one_of_one_le₀
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1

Tactic:
exact inv_le_one_of_one_le₀ ha

Premises used: inv_le_one_of_one_le₀