awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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‖
have rw : 1 ≤ ‖a‖⁻¹ * ‖r‖
Tactic: rw [norm_smul, norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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‖
⊢ (fun (x : E) ↦ a • x) y ∈ r • s
have h'' : 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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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‖
⊢ (fun (x : E) ↦ a • x) y ∈ r • s
have h' : y ∈ (a⁻¹ • r) • s
Tactic: have h' := hy (a⁻¹ • r) h''
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ (fun (x : E) ↦ a • x) y ∈ r • s
have inr : ∀ (h' : y ∈ a⁻¹ • r • s), (fun (x : E) ↦ a • x) y ∈ r • s
Tactic: rwa [smul_assoc, mem_inv_smul_set_iff₀ h] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ (fun (x : E) ↦ a • x) y ∈ r • s
have inr₁ : ∀ (h' : a • y ∈ r • s), (fun (x : E) ↦ a • x) y ∈ r • s
Tactic: rwa [smul_assoc, mem_inv_smul_set_iff₀ h] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have refine : ∀ (x : E) (hx : x ∈ t) (r : 𝕜) (hr : 1 ≤ ‖r‖), x ∈ r • s
Tactic: refine fun x hx => mem_balancedCoreAux_iff.2 fun r hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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‖
⊢ x ∈ r • s
have rw : r⁻¹ • x ∈ s
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp <| zero_lt_one.trans_le hr)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have refine : ‖r⁻¹‖ ≤ 1
Tactic: refine h (ht.smul_mem ?_ hx)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have rw : ‖r‖⁻¹ ≤ 1
Tactic: rw [norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have refine : balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s
Tactic: refine balancedCore_subset_balancedCoreAux.antisymm ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have refine : 0 ∈ balancedCoreAux 𝕜 s
Tactic: refine (balancedCoreAux_balanced ?_).subset_balancedCore_of_subset (balancedCoreAux_subset s)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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 ⊆ balancedCore 𝕜 t
have rw : s ⊆ ⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • t
Tactic: rw [balancedCore_eq_iInter ht]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have refine : ∀ (a : 𝕜) (ha : 1 ≤ ‖a‖), s ⊆ a • t
Tactic: refine subset_iInter₂ fun a ha ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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‖
⊢ s ⊆ a • t
have rw : a⁻¹ • s ⊆ t
Tactic: rw [subset_smul_set_iff₀ (norm_pos_iff.mp <| zero_lt_one.trans_le ha)]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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⁻¹ • s ⊆ t
have a₁ : ‖a⁻¹‖ ≤ 1
Tactic: apply hst
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have a₁ : ‖a‖⁻¹ ≤ 1
Tactic: rw [norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ IsClosed[inst_3] (balancedCore 𝕜 U)
have pos : ∀ (h : 0 ∈ U), IsClosed[inst_3] (balancedCore 𝕜 U)
Tactic: by_cases h : (0 : E) ∈ U
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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)
⊢ IsClosed[inst_3] (balancedCore 𝕜 U)
have neg : ∀ (h : 0 ∉ U), IsClosed[inst_3] (balancedCore 𝕜 U)
Tactic: by_cases h : (0 : E) ∈ U
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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] (balancedCore 𝕜 U)
have pos : IsClosed[inst_3] (⋂ (r : 𝕜), ⋂ (_ : 1 ≤ ‖r‖), r • U)
Tactic: rw [balancedCore_eq_iInter h]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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)
have pos : ∀ (a : 𝕜), IsClosed[inst_3] (⋂ (_ : 1 ≤ ‖a‖), a • U)
Tactic: refine isClosed_iInter fun a => ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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)
have pos : ∀ (ha : 1 ≤ ‖a‖), IsClosed[inst_3] (a • U)
Tactic: refine isClosed_iInter fun ha => ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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‖
⊢ IsClosed[inst_3] (a • U)
have ha' : 0 < ‖a‖
Tactic: have ha' := lt_of_lt_of_le zero_lt_one ha
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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‖
⊢ IsClosed[inst_3] (a • U)
have ha'₁ : a ≠ 0
Tactic: rw [norm_pos_iff] at ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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 = ∅
have contrapose! : ∀ (h : (balancedCore 𝕜 U).Nonempty), 0 ∈ U
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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] (balancedCore 𝕜 U)
have this : balancedCore 𝕜 U = ∅
Tactic: have : balancedCore 𝕜 U = ∅ := by
      contrapose! h
      exact balancedCore_nonempty_iff.mp h
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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] (balancedCore 𝕜 U)
have neg : IsClosed[inst_3] ∅
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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), 0 < r ∧ Membership.mem (γ := Filter E) (𝓝 0) V ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
have h : 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 _)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ Membership.mem (γ := Filter E) (𝓝 0) (balancedCore 𝕜 U)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ Membership.mem (γ := Filter E) (𝓝 0) (balancedCore 𝕜 U)
have obtain : ∀ (y : 𝕜) (hyr : ‖y‖ < r) (hy₀ : y ≠ 0), 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
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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) (balancedCore 𝕜 U)
have this : Membership.mem (γ := Filter E) (𝓝 0) (y • V)
Tactic: have : y • V ∈ 𝓝 (0 : E) := (set_smul_mem_nhds_zero_iff hy₀).mpr hV
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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)
have refine : ∀ (a : 𝕜) (ha : ‖a‖ ≤ 1), a • y • V ⊆ U
Tactic: refine Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => ?_)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ a • y • V ⊆ U
have rw : (a * y) • V ⊆ U
Tactic: rw [smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have refine : ‖a * y‖ < r
Tactic: refine hrVU _ _ ?_ hz
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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‖ < r
have rw : ‖a‖ * ‖y‖ < 1 * r
Tactic: rw [norm_mul, ← one_mul r]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have 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
Tactic: refine
    (closed_nhds_basis 0).to_hasBasis (fun s hs => ?_) fun s hs => ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
have refine : IsClosed[inst_3] (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)
Tactic: refine ⟨balancedCore 𝕜 s, ⟨balancedCore_mem_nhds_zero hs.1, ?_⟩, balancedCore_subset s⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
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) → ℝ))
have rw : Continuous[inst_3, _] (⇑(⨆ (i : ι), p i) : (a : E) → ℝ)
Tactic: rw [← Seminorm.coe_iSup_eq bdd]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
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) → ℝ)
have refine : LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⇑(⨆ (i : ι), p i) : (a : E) → ℝ)
Tactic: refine Seminorm.continuous_of_lowerSemicontinuous _ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
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)
⊢ LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⇑(⨆ (i : ι), p i) : (a : E) → ℝ)
have rw : LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))
Tactic: rw [Seminorm.coe_iSup_eq bdd]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (hypothesis)
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)
⊢ LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))
have bdd₁ : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
Tactic: rw [Seminorm.bddAbove_range_iff] at bdd
Cleared hypotheses: bdd
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
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 : ∀ (x : E), BddAbove (α := ℝ) (range fun (i : ι) ↦ (p i : (a : E) → ℝ) x)
⊢ LowerSemicontinuous.{u_3, 0} (α := E) (β := ℝ) (⨆ (i : ι), (⇑(p i) : (a : E) → ℝ))
have h : ∀ (x : E), Eq (α := ℝ) ((⨆ (i : ι), (⇑(p i) : (a : E) → ℝ)) x) (⨆ (i : ι), (p i : (a : E) → ℝ) x)
Tactic: convert! lowerSemicontinuous_ciSup (f := fun i x ↦ p i x) bdd (fun i ↦ (hp i).lowerSemicontinuous)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
⊢ Continuous[inst_7, _] (⇑p : (a : E) → ℝ)
have h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
Tactic: have h₁ : ∀ n : ℕ, IsClosed (p.closedBall (0 : E) n) := fun n ↦ by
      simpa [p.closedBall_zero_eq] using hp.isClosed_preimage n
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
⊢ Continuous[inst_7, _] (⇑p : (a : E) → ℝ)
have h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
Tactic: have h₂ : (⋃ n : ℕ, p.closedBall (0 : E) n) = univ :=
      eq_univ_of_forall fun x ↦ mem_iUnion.mpr (exists_nat_ge <| p (x - 0))
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.Barrelled (goal)
Goal:
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst : NontriviallyNormedField 𝕜₁
inst_1 : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst_2 : RingHomIsometric σ₁₂
inst_3 : AddCommGroup E
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₁ E
inst_6 : Module 𝕜₂ F
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : ContinuousConstSMul 𝕜₁ E
inst_10 : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)
h₁ : ∀ (n : ℕ), IsClosed[inst_7] (p.closedBall 0 (↑n : ℝ))
h₂ : Eq.{u_6 + 1} (α := Set E) (⋃ (n : ℕ), p.closedBall 0 (↑n : ℝ)) univ
⊢ Continuous[inst_7, _] (⇑p : (a : E) → ℝ)
have rcases : ∀ (n : ℕ) (x : E) (hxn : x ∈ interior (p.closedBall 0 (↑n : ℝ))), Continuous[inst_7, _] (⇑p : (a : E) → ℝ)
Tactic: rcases nonempty_interior_of_iUnion_of_closed h₁ h₂ with ⟨n, ⟨x, hxn⟩⟩