awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
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
⊢ (fun (x : E) ↦ r • x) y ∈ segment ℝ y (-y)
have a : ((1 + r) / 2) • y + ((1 - r) / 2) • -y = (fun (x : E) ↦ r • x) y
Tactic: refine ⟨(1 + r)/2, (1 - r)/2, by positivity, by positivity, by ring, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
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) • y + ((1 - r) / 2) • -y = (fun (x : E) ↦ r • x) y
have a : ((1 + r) / 2 - (1 - r) / 2) • y = (fun (x : E) ↦ r • x) y
Tactic: rw [smul_neg, ← sub_eq_add_neg, ← sub_smul]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
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)
    ((absConvexHull ℝ : (a : Set E) → Set E) s : Set E)
have rw : Eq (α := Set E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s) : Set E)
  ((convexHull ℝ : (a : Set E) → Set E) (balancedHull ℝ s) : Set E)
Tactic: rw [absConvexHull_eq_convexHull_balancedHull]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
h : x ∈ -s
⊢ x ∈ balancedHull ℝ s
have rw : ∃ (r : ℝ), ‖r‖ ≤ 1 ∧ x ∈ r • s
Tactic: rw [mem_balancedHull_iff]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
Goal:
E : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
s : Set E
x : E
h : x ∈ -s
⊢ ∃ (r : ℝ), ‖r‖ ≤ 1 ∧ x ∈ r • s
have h : norm (E := ℝ) (-1) ≤ 1 ∧ x ∈ HSMul.hSMul (α := ℝ) (-1) s
Tactic: use -1
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
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) (s ∪ -s) : Set E)
have 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)
Tactic: rw [← Convex.convexHull_eq (convex_convexHull ℝ (s ∪ -s))]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
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.{u_2} (α := E) ((absConvexHull ℝ : (a : Set E) → Set E) s)
have rw : TotallyBounded.{u_2} (α := E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s))
Tactic: rw [← convexHull_union_neg_eq_absConvexHull]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
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.{u_2} (α := E) ((convexHull ℝ : (a : Set E) → Set E) (s ∪ -s))
have hs₁ : TotallyBounded (s ∪ -s)
Tactic: apply totallyBounded_convexHull
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
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 ∪ -s)
have hs₁ : TotallyBounded s ∧ TotallyBounded (-s)
Tactic: rw [totallyBounded_union]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvex (goal)
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
⊢ IsCompact.{u_3} (X := E) ((closedAbsConvexHull ℝ : (a : Set E) → Set E) s)
have rw : IsCompact.{u_3} (X := E) (closure[inst_2.toTopologicalSpace] ((absConvexHull ℝ : (a : Set E) → Set E) s))
Tactic: rw [closedAbsConvexHull_eq_closure_absConvexHull]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : SeminormedRing 𝕜
inst_3 : SMul 𝕜 E
inst_4 : PartialOrder 𝕜
⊢ Nonempty.{u_2 + 1} (AbsConvexOpenSets 𝕜 E)
have rw : ∃ (x : AbsConvexOpenSets 𝕜 E), True
Tactic: rw [← exists_true_iff_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : TopologicalSpace E
inst_1 : AddCommMonoid E
inst_2 : SeminormedRing 𝕜
inst_3 : SMul 𝕜 E
inst_4 : PartialOrder 𝕜
⊢ ∃ (x : { s : Set E // 0 ∈ s ∧ IsOpen[inst] s ∧ AbsConvex 𝕜 s }), True
have rw : ∃ (a : Set E) (_ : 0 ∈ a ∧ IsOpen[inst] a ∧ AbsConvex 𝕜 a), True
Tactic: rw [Subtype.exists]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ (gaugeSeminorm (s := (↑s : Set E)) ⋯ ⋯ ⋯).ball 0 1 = (↑s : Set E)
have rw : {y : E | LT.lt (α := ℝ) ((gaugeSeminorm (s := (↑s : Set E)) sorry sorry sorry : (a : E) → ℝ) y : ℝ) (1 : ℝ)} = (↑s : Set E)
Tactic: rw [Seminorm.ball_zero_eq]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
⊢ WithSeminorms (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)
have refine : Filter.HasBasis (𝓝 0)
  (fun (s : Set E) ↦ s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)) id
Tactic: refine SeminormFamily.withSeminorms_of_hasBasis _ ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
⊢ Filter.HasBasis (𝓝 0)
    (fun (s : Set E) ↦ s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)) id
have refine_1 : ∀ (s : Set E) (hs : 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s),
  ∃ i' ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E), id i' ⊆ id s
Tactic: refine (nhds_hasBasis_absConvex_open 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs => ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
refine_1 :
  ∀ (s : Set E) (hs : 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s),
    ∃ i' ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E), id i' ⊆ id s
⊢ Filter.HasBasis (𝓝 0)
    (fun (s : Set E) ↦ s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)) id
have refine_2 : ∀ (s : Set E) (hs : s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)),
  ∃ (i : Set E), (0 ∈ i ∧ IsOpen[inst_2] i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s
Tactic: refine (nhds_hasBasis_absConvex_open 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs => ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
s : Set E
hs : 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s
⊢ ∃ i' ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E), id i' ⊆ id s
have refine_1 : s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)
Tactic: refine ⟨s, ⟨?_, rfl.subset⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
s : Set E
hs : 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s
⊢ s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)
have h : s =
  Seminorm.ball
    (gaugeSeminormFamily 𝕜 E (Subtype.mk (p := fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s) s hs)) 0 1
Tactic: convert! (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
s : Set E
hs : 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s
⊢ s =
    Seminorm.ball
      (gaugeSeminormFamily 𝕜 E (Subtype.mk (p := fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s) s hs)) 0 1
have h : s = (↑(Subtype.mk (p := fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s) s hs) : Set E)
Tactic: rw [gaugeSeminormFamily_ball, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
s : Set E
hs : 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s
h : s = (↑(Subtype.mk (p := fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s) s hs) : Set E)
⊢ s =
    Seminorm.ball
      (gaugeSeminormFamily 𝕜 E (Subtype.mk (p := fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s) s hs)) 0 1
have h₁ : s = s
Tactic: rw [gaugeSeminormFamily_ball, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
s : Set E
hs : s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)
⊢ ∃ (i : Set E), (0 ∈ i ∧ IsOpen[inst_2] i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s
have refine_2 : 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s
Tactic: refine ⟨s, ⟨?_, rfl.subset⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
s : Set E
hs : s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)
⊢ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s
have hs₁ : ∃ (i : Finset (AbsConvexOpenSets 𝕜 E)) (r : ℝ), 0 < r ∧ s = (i.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r
Tactic: rw [SeminormFamily.basisSets_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
s : Set E
hs : ∃ (i : Finset (AbsConvexOpenSets 𝕜 E)) (r : ℝ), 0 < r ∧ s = (i.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r
⊢ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s
have refine_2 : ∀ (t : Finset (AbsConvexOpenSets 𝕜 E)) (r : ℝ) (hr : 0 < r),
  0 ∈ (t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r ∧
    IsOpen[inst_2] ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r) ∧
      AbsConvex 𝕜 ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r)
Tactic: rcases hs with ⟨t, r, hr, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ (t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r ∧
    IsOpen[inst_2] ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r) ∧
      AbsConvex 𝕜 ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r)
have refine_2 : Membership.mem (γ := Set E) (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) 0 ∧
  IsOpen[inst_2] (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) ∧
    AbsConvex.{u_1, u_2} 𝕜 (E := E) (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r)
Tactic: rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ Membership.mem (γ := Set E) (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) 0 ∧
    IsOpen[inst_2] (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) ∧
      AbsConvex.{u_1, u_2} 𝕜 (E := E) (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r)
have refine_2 : ∀ S ∈ t, IsOpen[inst_2] ((gaugeSeminormFamily 𝕜 E S).ball 0 r)
Tactic: refine
    ⟨mem_iInter₂.mpr fun _ _ => by simp [hr],
      isOpen_biInter_finset fun S _ => ?_,
      balanced_iInter₂ fun _ _ => Seminorm.balanced_ball_zero _ _,
      convex_iInter₂ fun _ _ => (convex_of_nonneg_surjective_algebraMap _
        (fun _ => RCLike.nonneg_iff_exists_ofReal.mp) (Seminorm.convex_ball _ _ _) ..)⟩
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
h : S ∈ t
⊢ IsOpen[inst_2] ((gaugeSeminormFamily 𝕜 E S).ball 0 r)
have hr' : r = norm.{u_1} (E := 𝕜) (↑r : 𝕜) * 1
Tactic: have hr' : r = ‖(r : 𝕜)‖ * 1 := by simp [abs_of_pos hr]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
h : S ∈ t
hr' : r = norm.{u_1} (E := 𝕜) (↑r : 𝕜) * 1
⊢ IsOpen[inst_2] ((gaugeSeminormFamily 𝕜 E S).ball 0 r)
have hr'' : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
Tactic: have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.AbsConvexOpen (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : Module ℝ E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : ContinuousSMul ℝ E
inst_7 : IsTopologicalAddGroup E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : LocallyConvexSpace 𝕜 E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
h : S ∈ t
hr' : r = norm.{u_1} (E := 𝕜) (↑r : 𝕜) * 1
hr'' : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
⊢ IsOpen[inst_2] ((gaugeSeminormFamily 𝕜 E S).ball 0 r)
have refine_2 : IsOpen[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) (↑S : Set E))
Tactic: rw [hr', ← Seminorm.smul_ball_zero hr'', gaugeSeminormFamily_ball]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
x : E
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
have simp_rw : Membership.mem (γ := Set E) (⋃₀ {t : Set E | Balanced 𝕜 t ∧ t ⊆ s}) x ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
Tactic: simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
x : E
simp_rw :
  Membership.mem (γ := Set E) (⋃₀ {t : Set E | Balanced 𝕜 t ∧ t ⊆ s}) x ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
have simp_rw₁ : (∃ (t : Set E), Membership.mem (γ := Set (Set E)) {t : Set E | Balanced 𝕜 t ∧ t ⊆ s} t ∧ x ∈ t) ↔
  ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
Tactic: simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
x : E
simp_rw :
  Membership.mem (γ := Set E) (⋃₀ {t : Set E | Balanced 𝕜 t ∧ t ⊆ s}) x ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
simp_rw₁ :
  (∃ (t : Set E), Membership.mem (γ := Set (Set E)) {t : Set E | Balanced 𝕜 t ∧ t ⊆ s} t ∧ x ∈ t) ↔
    ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
have simp_rw₂ : (∃ (t : Set E), (Balanced 𝕜 t ∧ t ⊆ s) ∧ x ∈ t) ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
Tactic: simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCore 𝕜 s
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCore 𝕜 s
have hy₁ : ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t
Tactic: rw [mem_balancedCore_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCore 𝕜 s
have rcases : ∀ (t : Set E) (ht1 : Balanced 𝕜 t) (ht2 : t ⊆ s) (hy : y ∈ t), (fun (x : E) ↦ a • x) y ∈ balancedCore 𝕜 s
Tactic: rcases hy with ⟨t, ht1, ht2, hy⟩
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ x ∈ t
have 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
Tactic: obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ x ∈ balancedHull 𝕜 t
have rw : ∀ (hx : ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • s), ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • t
Tactic: rw [mem_balancedHull_iff] at *
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • t
have obtain : ∀ (r : 𝕜) (hr₁ : ‖r‖ ≤ 1) (hr₂ : x ∈ r • s), ∃ (r : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • t
Tactic: obtain ⟨r, hr₁, hr₂⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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 : 𝕜), ‖r‖ ≤ 1 ∧ x ∈ r • t
have h : ‖r‖ ≤ 1 ∧ x ∈ r • t
Tactic: use r
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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
⊢ 0 ∈ s
have hs_nonempty₁ : (balancedCore 𝕜 s).Nonempty
Tactic: rw [← hs.balancedCore_eq] at hs_nonempty
Cleared hypotheses: hs_nonempty
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (goal)
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
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s
have simp_rw : ∀ (x : E), (∃ (i : 𝕜) (_ : ‖i‖ ≤ 1), x ∈ a • i • s) → ∃ (i : 𝕜) (_ : ‖i‖ ≤ 1), x ∈ i • s
Tactic: simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.BalancedCoreHull (hypothesis)
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
have hx₁ : x ∈ (a • r) • s
Tactic: rw [← smul_assoc] at hx
Cleared hypotheses: 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
⊢ Eq.{u_2 + 1} (α := Set E) (balancedCoreAux 𝕜 ∅) ∅
have simp_rw : ∀ (a : E), ∃ (i : 𝕜) (_ : 1 ≤ ‖i‖), a ∉ ∅
Tactic: simp_rw [balancedCoreAux, iInter₂_eq_empty_iff, smul_set_empty]
-- 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 : y ∈ balancedCoreAux 𝕜 s
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCoreAux 𝕜 s
have inl : ∀ (ha : norm.{u_1} (E := 𝕜) 0 ≤ 1), (fun (x : E) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) y ∈ balancedCoreAux 𝕜 s
Tactic: obtain rfl | h := eq_or_ne a 0
Cleared hypotheses: 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 : 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
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCoreAux 𝕜 s
have inr : ∀ (h : a ≠ 0), (fun (x : E) ↦ a • x) y ∈ balancedCoreAux 𝕜 s
Tactic: obtain rfl | h := eq_or_ne a 0
-- 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 : y ∈ balancedCoreAux 𝕜 s
h : a ≠ 0
⊢ (fun (x : E) ↦ a • x) y ∈ balancedCoreAux 𝕜 s
have inr : ∀ (hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s) (h : a ≠ 0) (r : 𝕜), 1 ≤ ‖r‖ → (fun (x : E) ↦ a • x) y ∈ r • s
Tactic: rw [mem_balancedCoreAux_iff] at hy ⊢
Cleared hypotheses: hy, h