awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvex
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : UniformSpace E
inst_3 : IsUniformAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
inst_6 : QuasiCompleteSpace ℝ E
s : Set E
ht : TotallyBounded s
⊢ IsCompact.{u_3} (X := E) (closure[inst_2.toTopologicalSpace] ((absConvexHull ℝ : (a : Set E) → Set E) s))

Tactic:
isCompact_closure_of_totallyBounded_quasiComplete (𝕜 := ℝ)
    (totallyBounded_absConvexHull E ht)

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

Tactic:
exact isCompact_closure_of_totallyBounded_quasiComplete (𝕜 := ℝ)
    (totallyBounded_absConvexHull E ht)

Premises used: totallyBounded_absConvexHull, isCompact_closure_of_totallyBounded_quasiComplete
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
s : AbsConvexOpenSets 𝕜 E
⊢ 0 ∈ (↑s : Set E)

Tactic:
s.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
s : AbsConvexOpenSets 𝕜 E
⊢ IsOpen[inst] (↑s : Set E)

Tactic:
s.2.2.1

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
s : AbsConvexOpenSets 𝕜 E
⊢ Membership.mem (γ := Filter E) (𝓝 0) (↑s : Set E)

Tactic:
s.coe_isOpen.mem_nhds s.coe_zero_mem

Premises used: AbsConvexOpenSets.coe_isOpen, IsOpen.mem_nhds, AbsConvexOpenSets.coe_zero_mem
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
s : AbsConvexOpenSets 𝕜 E
⊢ Balanced 𝕜 (↑s : Set E)

Tactic:
s.2.2.2.1

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
s : AbsConvexOpenSets 𝕜 E
⊢ Convex 𝕜 (↑s : Set E)

Tactic:
s.2.2.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
rw : ∃ (x : AbsConvexOpenSets 𝕜 E), True
⊢ Nonempty.{u_2 + 1} (AbsConvexOpenSets 𝕜 E)

Tactic:
rw [← exists_true_iff_nonempty]

Premises used: exists_true_iff_nonempty
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
rw : ∃ (a : Set E) (_ : 0 ∈ a ∧ IsOpen[inst] a ∧ AbsConvex 𝕜 a), True
⊢ ∃ (x : { s : Set E // 0 ∈ s ∧ IsOpen[inst] s ∧ AbsConvex 𝕜 s }), True

Tactic:
rw [Subtype.exists]

Premises used: Subtype.exists
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
⊢ ∃ (a : Set E) (_ : 0 ∈ a ∧ IsOpen[inst] a ∧ AbsConvex 𝕜 a), True

Tactic:
⟨Set.univ, ⟨mem_univ 0, isOpen_univ, balanced_univ, convex_univ⟩, trivial⟩

Premises used: trivial, Set.univ, isOpen_univ, convex_univ, And.intro, Exists.intro, Set.mem_univ, balanced_univ, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 𝕜
⊢ ∃ (a : Set E) (_ : 0 ∈ a ∧ IsOpen[inst] a ∧ AbsConvex 𝕜 a), True

Tactic:
exact ⟨Set.univ, ⟨mem_univ 0, isOpen_univ, balanced_univ, convex_univ⟩, trivial⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
rw : {y : E | LT.lt (α := ℝ) ((gaugeSeminorm (s := (↑s : Set E)) ⋯ ⋯ ⋯ : (a : E) → ℝ) y : ℝ) (1 : ℝ)} = (↑s : Set E)
⊢ (gaugeSeminorm (s := (↑s : Set E)) ⋯ ⋯ ⋯).ball 0 1 = (↑s : Set E)

Tactic:
rw [Seminorm.ball_zero_eq]

Premises used: Seminorm.ball_zero_eq
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
⊢ {y : E | gauge (↑s : Set E) y < 1} = (↑s : Set E)

Tactic:
gauge_lt_one_eq_self_of_isOpen (s.coe_convex.lift ℝ) s.coe_zero_mem s.coe_isOpen

Premises used: gauge_lt_one_eq_self_of_isOpen, Real, AbsConvexOpenSets.coe_isOpen, Convex.lift, AbsConvexOpenSets.coe_zero_mem, AbsConvexOpenSets.coe_convex
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
⊢ {y : E | gauge (↑s : Set E) y < 1} = (↑s : Set E)

Tactic:
exact gauge_lt_one_eq_self_of_isOpen (s.coe_convex.lift ℝ) s.coe_zero_mem s.coe_isOpen

Premises used: gauge_lt_one_eq_self_of_isOpen, Real, AbsConvexOpenSets.coe_isOpen, Convex.lift, AbsConvexOpenSets.coe_zero_mem, AbsConvexOpenSets.coe_convex
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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)

Tactic:
SeminormFamily.withSeminorms_of_hasBasis _ ?_

Premises used: SeminormFamily.withSeminorms_of_hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 :
  Filter.HasBasis (𝓝 0)
    (fun (s : Set E) ↦ s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)) id
⊢ WithSeminorms (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)

Tactic:
refine SeminormFamily.withSeminorms_of_hasBasis _ ?_

Premises used: SeminormFamily.withSeminorms_of_hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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

Tactic:
(nhds_hasBasis_absConvex_open 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs => ?_

Premises used: nhds_hasBasis_absConvex_open, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
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
⊢ Filter.HasBasis (𝓝 0)
    (fun (s : Set E) ↦ s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)) id

Tactic:
refine (nhds_hasBasis_absConvex_open 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs => ?_

Premises used: nhds_hasBasis_absConvex_open, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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

Tactic:
⟨s, ⟨?_, rfl.subset⟩⟩

Premises used: Eq.subset, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
refine_1 : s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)
⊢ ∃ i' ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E), id i' ⊆ id s

Tactic:
refine ⟨s, ⟨?_, rfl.subset⟩⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
⊢ Seminorm.ball
      (gaugeSeminormFamily 𝕜 E (Subtype.mk (p := fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s) s hs)) 0
      1 ∈
    SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)

Tactic:
(gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos

Premises used: gaugeSeminormFamily, Subtype.mk, SeminormFamily.basisSets_singleton_mem, one_pos
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 =
    Seminorm.ball
      (gaugeSeminormFamily 𝕜 E (Subtype.mk (p := fun (s : Set E) ↦ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s) s hs)) 0 1
⊢ s ∈ SeminormFamily.basisSets (ι := AbsConvexOpenSets 𝕜 E) (gaugeSeminormFamily 𝕜 E)

Tactic:
convert! (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos

Premises used: gaugeSeminormFamily, Subtype.mk, SeminormFamily.basisSets_singleton_mem, one_pos
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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)
h₁ h₂ : s = 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

Tactic:
rw [gaugeSeminormFamily_ball, Subtype.coe_mk]

Premises used: Subtype.coe_mk, gaugeSeminormFamily_ball
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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

Tactic:
⟨s, ⟨?_, rfl.subset⟩⟩

Premises used: Eq.subset, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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)
refine_2 : 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s
⊢ ∃ (i : Set E), (0 ∈ i ∧ IsOpen[inst_2] i ∧ AbsConvex 𝕜 i) ∧ id i ⊆ id s

Tactic:
refine ⟨s, ⟨?_, rfl.subset⟩⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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 : Finset (AbsConvexOpenSets 𝕜 E)) (r : ℝ), 0 < r ∧ s = (i.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r

Tactic:
rw [SeminormFamily.basisSets_iff] at hs

Premises used: SeminormFamily.basisSets_iff
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
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)
⊢ 0 ∈ s ∧ IsOpen[inst_2] s ∧ AbsConvex 𝕜 s

Tactic:
rcases hs with ⟨t, r, hr, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
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)
⊢ 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:
rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]

Premises used: Seminorm.ball_finset_sup_eq_iInter
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
x : AbsConvexOpenSets 𝕜 E
h : x ∈ t
⊢ 0 ∈ (gaugeSeminormFamily 𝕜 E x).ball 0 r

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
refine_2 : ∀ S ∈ t, IsOpen[inst_2] ((gaugeSeminormFamily 𝕜 E S).ball 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)

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 _ _ _) ..)⟩
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
⊢ r = norm.{u_1} (E := 𝕜) (↑r : 𝕜) * 1

Tactic:
simp [abs_of_pos hr]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
⊢ r = norm.{u_1} (E := 𝕜) (↑r : 𝕜) * 1

Tactic:
have hr' : r = ‖(r : 𝕜)‖ * 1 := by simp [abs_of_pos hr]
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0

Tactic:
simp [hr.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0

Tactic:
have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
refine_2 : IsOpen[inst_2] (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) (↑S : Set E))
⊢ IsOpen[inst_2] ((gaugeSeminormFamily 𝕜 E S).ball 0 r)

Tactic:
rw [hr', ← Seminorm.smul_ball_zero hr'', gaugeSeminormFamily_ball]

Premises used: Seminorm.smul_ball_zero, gaugeSeminormFamily_ball
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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] (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) (↑S : Set E))

Tactic:
S.coe_isOpen.smul₀ hr''

Premises used: AbsConvexOpenSets.coe_isOpen, IsOpen.smul₀
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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] (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑r : 𝕜) (↑S : Set E))

Tactic:
exact S.coe_isOpen.smul₀ hr''

Premises used: AbsConvexOpenSets.coe_isOpen, IsOpen.smul₀
-- Module: Mathlib.Analysis.LocallyConvex.AbsConvexOpen
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
⊢ PolynormableSpace 𝕜 E

Tactic:
with_gaugeSeminormFamily.toPolynormableSpace

Premises used: with_gaugeSeminormFamily, WithSeminorms.toPolynormableSpace
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
s : Set E
⊢ balancedCore 𝕜 s ⊆ s

Tactic:
sUnion_subset fun _ ht => ht.2

Premises used: Set.sUnion_subset, And.right, balancedCore
-- Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedRing 𝕜
inst_1 : SMul 𝕜 E
⊢ Eq.{u_2 + 1} (α := Set E) (balancedCore 𝕜 ∅) ∅

Tactic:
eq_empty_of_subset_empty (balancedCore_subset _)

Premises used: Set.eq_empty_of_subset_empty, balancedCore_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
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
simp_rw₂ : (∃ (t : Set E), (Balanced 𝕜 t ∧ t ⊆ s) ∧ x ∈ t) ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

Tactic:
simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]

Premises used: Set.mem_setOf_eq, and_assoc, balancedCore, Set.mem_sUnion
-- 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 : y ∈ balancedCore 𝕜 s
⊢ ∃ (t : Set E), Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t

Tactic:
rw [mem_balancedCore_iff] at hy

Premises used: mem_balancedCore_iff