awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
pos : ∀ (h : 0 ∈ U), IsClosed[inst_3] (balancedCore 𝕜 U)
neg : ∀ (h : 0 ∉ U), IsClosed[inst_3] (balancedCore 𝕜 U)
⊢ IsClosed[inst_3] (balancedCore 𝕜 U)

Tactic:
by_cases h : (0 : E) ∈ U

Premises used: 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
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
pos : IsClosed[inst_3] (⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • U)
⊢ IsClosed[inst_3] (balancedCore 𝕜 U)

Tactic:
rw [balancedCore_eq_iInter h]

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
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
⊢ IsClosed[inst_3] (⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • U)

Tactic:
isClosed_iInter fun a => ?_

Premises used: isClosed_iInter
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
pos : ∀ (a : 𝕜), IsClosed[inst_3] (⋂ (_ : 1 ≤ ‖a‖), a • U)
⊢ IsClosed[inst_3] (⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • U)

Tactic:
refine isClosed_iInter fun a => ?_

Premises used: isClosed_iInter
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
a : 𝕜
⊢ IsClosed[inst_3] (⋂ (_ : 1 ≤ ‖a‖), a • U)

Tactic:
isClosed_iInter fun ha => ?_

Premises used: isClosed_iInter
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
a : 𝕜
pos : ∀ (ha : 1 ≤ ‖a‖), IsClosed[inst_3] (a • U)
⊢ IsClosed[inst_3] (⋂ (_ : 1 ≤ ‖a‖), a • U)

Tactic:
refine isClosed_iInter fun ha => ?_

Premises used: isClosed_iInter
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ 0 < ‖a‖

Tactic:
have ha' := lt_of_lt_of_le zero_lt_one ha
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : 0 < ‖a‖
⊢ a ≠ 0

Tactic:
rw [norm_pos_iff] at ha'

Premises used: norm_pos_iff
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : a ≠ 0
⊢ IsClosed[inst_3] (a • U)

Tactic:
isClosedMap_smul_of_ne_zero ha' U hU

Premises used: isClosedMap_smul_of_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : a ≠ 0
⊢ IsClosed[inst_3] (a • U)

Tactic:
exact isClosedMap_smul_of_ne_zero ha' U hU

Premises used: isClosedMap_smul_of_ne_zero
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∉ U
contrapose! : ∀ (h : (balancedCore 𝕜 U).Nonempty), 0 ∈ U
⊢ balancedCore 𝕜 U = ∅

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : (balancedCore 𝕜 U).Nonempty
⊢ 0 ∈ U

Tactic:
balancedCore_nonempty_iff.mp h

Premises used: balancedCore_nonempty_iff, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : (balancedCore 𝕜 U).Nonempty
⊢ 0 ∈ U

Tactic:
exact balancedCore_nonempty_iff.mp h

Premises used: balancedCore_nonempty_iff, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∉ U
⊢ balancedCore 𝕜 U = ∅

Tactic:
have : balancedCore 𝕜 U = ∅ := by
      contrapose! h
      exact balancedCore_nonempty_iff.mp h
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∉ U
this : balancedCore 𝕜 U = ∅
neg : IsClosed[inst_3] ∅
⊢ IsClosed[inst_3] (balancedCore 𝕜 U)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∉ U
this : balancedCore 𝕜 U = ∅
⊢ IsClosed[inst_3] ∅

Tactic:
isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed[inst_3] U
h : 0 ∉ U
this : balancedCore 𝕜 U = ∅
⊢ IsClosed[inst_3] ∅

Tactic:
exact isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 (0, 0)) (𝓝 0)

Tactic:
have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
      continuous_smul.tendsto' (0, 0) _ (smul_zero _)
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h : Tendsto (β := E) (fun (x : 𝕜 × E) ↦ x.1 • x.2) (𝓝 (0, 0)) (𝓝 0)
⊢ ∃ (r : ℝ) (V : Set E), 0 < r ∧ Membership.mem (γ := Filter E) (𝓝 0) V ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U

Tactic:
simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using
      h.basis_left (NormedAddGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU

Premises used: Prod.exists', and_imp, nhds, exists_prop, Filter.basis_sets, Filter.HasBasis.prod_nhds, Filter.Tendsto.basis_left, and_assoc, Prod.forall', NormedAddGroup.nhds_zero_basis_norm_lt
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
obtain :
  ∀ (r : ℝ) (V : Set E) (hr : 0 < r) (hV : Membership.mem (γ := Filter E) (𝓝 0) V)
    (hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U), Membership.mem (γ := Filter E) (𝓝 0) (balancedCore 𝕜 U)
⊢ Membership.mem (γ := Filter E) (𝓝 0) (balancedCore 𝕜 U)

Tactic:
obtain ⟨r, V, hr, hV, hrVU⟩ : ∃ (r : ℝ) (V : Set E),
      0 < r ∧ V ∈ 𝓝 (0 : E) ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U := by
    have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
      continuous_smul.tendsto' (0, 0) _ (smul_zero _)
    simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using
      h.basis_left (NormedAddGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU

Premises used: nhds, OfNat.ofNat, Set
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
⊢ ∃ (y : 𝕜), ‖y‖ < r ∧ y ≠ 0

Tactic:
Filter.nonempty_of_mem <|
      (nhdsWithin_hasBasis NormedAddGroup.nhds_zero_basis_norm_lt {0}ᶜ).mem_of_mem hr

Premises used: Set.Mem, Compl.compl, Filter.nonempty_of_mem, Set.Nonempty, nhdsWithin_hasBasis, NormedAddGroup.nhds_zero_basis_norm_lt, Singleton.singleton, OfNat.ofNat, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
obtain : ∀ (y : 𝕜) (hyr : ‖y‖ < r) (hy₀ : y ≠ 0), Membership.mem (γ := Filter E) (𝓝 0) (balancedCore 𝕜 U)
⊢ Membership.mem (γ := Filter E) (𝓝 0) (balancedCore 𝕜 U)

Tactic:
obtain ⟨y, hyr, hy₀⟩ : ∃ y : 𝕜, ‖y‖ < r ∧ y ≠ 0 :=
    Filter.nonempty_of_mem <|
      (nhdsWithin_hasBasis NormedAddGroup.nhds_zero_basis_norm_lt {0}ᶜ).mem_of_mem hr

Premises used: Compl.compl, Filter.nonempty_of_mem, nhdsWithin_hasBasis, NormedAddGroup.nhds_zero_basis_norm_lt, Singleton.singleton, OfNat.ofNat, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
⊢ Membership.mem (γ := Filter E) (𝓝 0) (y • V)

Tactic:
have : y • V ∈ 𝓝 (0 : E) := (set_smul_mem_nhds_zero_iff hy₀).mpr hV
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
⊢ Membership.mem (γ := Filter E) (𝓝 0) (balancedCore 𝕜 U)

Tactic:
Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => ?_)

Premises used: subset_balancedCore, mem_of_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
refine : ∀ (a : 𝕜) (ha : ‖a‖ ≤ 1), a • y • V ⊆ U
⊢ Membership.mem (γ := Filter E) (𝓝 0) (balancedCore 𝕜 U)

Tactic:
refine Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => ?_)

Premises used: subset_balancedCore, mem_of_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
a : 𝕜
ha : ‖a‖ ≤ 1
rw : (a * y) • V ⊆ U
⊢ a • y • V ⊆ U

Tactic:
rw [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ (fun (x : E) ↦ (a * y) • x) z ∈ U

Tactic:
hrVU _ _ ?_ hz

Premises used: Set.Mem
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
refine : ‖a * y‖ < r
⊢ (fun (x : E) ↦ (a * y) • x) z ∈ U

Tactic:
refine hrVU _ _ ?_ hz
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
rw : ‖a‖ * ‖y‖ < 1 * r
⊢ ‖a * y‖ < r

Tactic:
rw [norm_mul, ← one_mul r]

Premises used: norm_mul, one_mul
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ ‖a‖ * ‖y‖ < 1 * r

Tactic:
mul_lt_mul' ha hyr (norm_nonneg y) one_pos

Premises used: mul_lt_mul', one_pos, norm_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
U : Set E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
hU : Membership.mem (γ := Filter E) (𝓝 0) U
r : ℝ
V : Set E
hr : 0 < r
hV : Membership.mem (γ := Filter E) (𝓝 0) V
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ ‖a‖ * ‖y‖ < 1 * r

Tactic:
exact mul_lt_mul' ha hyr (norm_nonneg y) one_pos

Premises used: mul_lt_mul', one_pos, norm_nonneg
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) s ∧ Balanced 𝕜 s) id

Tactic:
Filter.hasBasis_self.mpr fun s hs =>
    ⟨balancedCore 𝕜 s, balancedCore_mem_nhds_zero hs, balancedCore_balanced s,
      balancedCore_subset s⟩

Premises used: Iff.mpr, balancedCore_mem_nhds_zero, And.intro, Exists.intro, balancedCore, balancedCore_balanced, Filter.hasBasis_self, 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
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_6 : RegularSpace E
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) s ∧ IsClosed[inst_3] s ∧ Balanced 𝕜 s) id

Tactic:
(closed_nhds_basis 0).to_hasBasis (fun s hs => ?_) fun s hs => ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩

Premises used: closed_nhds_basis, Eq.subset, And.right, And.left, And.intro, Exists.intro, OfNat.ofNat, Filter.HasBasis.to_hasBasis, rfl
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_6 : RegularSpace E
s :
  ∀ (s : Set E) (hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ IsClosed[inst_3] s),
    ∃ (i' : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i' ∧ IsClosed[inst_3] i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s
⊢ HasBasis (𝓝 0) (fun (s : Set E) ↦ Membership.mem (γ := Filter E) (𝓝 0) s ∧ IsClosed[inst_3] s ∧ Balanced 𝕜 s) id

Tactic:
refine
    (closed_nhds_basis 0).to_hasBasis (fun s hs => ?_) fun s hs => ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩

Premises used: closed_nhds_basis, Eq.subset, And.intro, Exists.intro, OfNat.ofNat, Filter.HasBasis.to_hasBasis, rfl
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_6 : RegularSpace E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ IsClosed[inst_3] s
⊢ ∃ (i' : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i' ∧ IsClosed[inst_3] i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s

Tactic:
⟨balancedCore 𝕜 s, ⟨balancedCore_mem_nhds_zero hs.1, ?_⟩, balancedCore_subset s⟩

Premises used: balancedCore_mem_nhds_zero, And.left, And.intro, Exists.intro, balancedCore, 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
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_6 : RegularSpace E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ IsClosed[inst_3] s
refine : IsClosed[inst_3] (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)
⊢ ∃ (i' : Set E), (Membership.mem (γ := Filter E) (𝓝 0) i' ∧ IsClosed[inst_3] i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s

Tactic:
refine ⟨balancedCore 𝕜 s, ⟨balancedCore_mem_nhds_zero hs.1, ?_⟩, balancedCore_subset s⟩
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_6 : RegularSpace E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ IsClosed[inst_3] s
⊢ IsClosed[inst_3] (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)

Tactic:
⟨hs.2.balancedCore, balancedCore_balanced s⟩

Premises used: And.right, IsClosed.balancedCore, And.intro, balancedCore_balanced
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousSMul 𝕜 E
inst_5 : NeBot (α := 𝕜) (𝓝[≠] 0)
inst_6 : RegularSpace E
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s ∧ IsClosed[inst_3] s
⊢ IsClosed[inst_3] (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)

Tactic:
exact ⟨hs.2.balancedCore, balancedCore_balanced s⟩
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
𝕜 : Type u_1
E : Type u_2
inst : AddGroup E
inst_1 : SMul 𝕜 E
inst_2 : SeminormedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : Seminorm 𝕜 E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
BarrelledSpace.continuous_of_lowerSemicontinuous p hp

Premises used: BarrelledSpace.continuous_of_lowerSemicontinuous
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : BddAbove (range p)
rw : Continuous[inst_3, _] (⇑(⨆ (i : ι), p i) : (a : E) → ℝ)
⊢ Continuous[inst_3, _] (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))

Tactic:
rw [← Seminorm.coe_iSup_eq bdd]

Premises used: Seminorm.coe_iSup_eq
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : BddAbove (range p)
⊢ Continuous[inst_3, _] (⇑(⨆ (i : ι), p i) : (a : E) → ℝ)

Tactic:
Seminorm.continuous_of_lowerSemicontinuous _ ?_

Premises used: Seminorm.continuous_of_lowerSemicontinuous
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : BddAbove (range p)
refine : LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⇑(⨆ (i : ι), p i) : (a : E) → ℝ)
⊢ Continuous[inst_3, _] (⇑(⨆ (i : ι), p i) : (a : E) → ℝ)

Tactic:
refine Seminorm.continuous_of_lowerSemicontinuous _ ?_

Premises used: Seminorm.continuous_of_lowerSemicontinuous
-- Module: Mathlib.Analysis.LocallyConvex.Barrelled
Goal:
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous[inst_3, _] (⇑(p i) : (a : E) → ℝ)
bdd : BddAbove (range p)
rw : LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))
⊢ LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⇑(⨆ (i : ι), p i) : (a : E) → ℝ)

Tactic:
rw [Seminorm.coe_iSup_eq bdd]

Premises used: Seminorm.coe_iSup_eq