awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
⊢ 0 < I.sup' hI r

Tactic:
have h' : 0 < I.sup' hI r := by
      rcases hI with ⟨i, hi⟩
      exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
h' : 0 < I.sup' hI r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
⟨I.sup' hI r, h', fun x hx => finset_sup_apply_lt h' fun i hi => ?_⟩

Premises used: Seminorm.finset_sup_apply_lt, And.intro, Exists.intro, Finset.sup'
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
h' : 0 < I.sup' hI r
pos : ∀ (x : E) (hx : x ∈ s) (i : ι) (hi : i ∈ I), (p i : (a : E) → ℝ) x < I.sup' hI r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
refine ⟨I.sup' hI r, h', fun x hx => finset_sup_apply_lt h' fun i hi => ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ (p i : (a : E) → ℝ) x < I.sup' hI r

Tactic:
lt_of_lt_of_le (h i x hx) ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
pos : r i ≤ I.sup' hI r
⊢ (p i : (a : E) → ℝ) x < I.sup' hI r

Tactic:
refine lt_of_lt_of_le (h i x hx) ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
pos : ∃ b ∈ I, r i ≤ r b
⊢ r i ≤ I.sup' hI r

Tactic:
simp only [Finset.le_sup'_iff]

Premises used: Finset.le_sup'_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ ∃ b ∈ I, r i ≤ r b

Tactic:
⟨i, hi, (Eq.refl _).le⟩

Premises used: Eq.le, And.intro, Exists.intro, Eq.refl
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : (i : ι) → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i : (a : E) → ℝ) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ ∃ b ∈ I, r i ≤ r b

Tactic:
exact ⟨i, hi, (Eq.refl _).le⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
I : Finset ι
hI : I = ∅
neg : ∃ r > 0, ∀ x ∈ s, 0 < r
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p : (a : E) → ℝ) x < r

Tactic:
simp only [hI, Finset.sup_empty, coe_bot, Pi.zero_apply]

Premises used: Pi.zero_apply, Finset.sup_empty, Seminorm.coe_bot
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
I : Finset ι
hI : I = ∅
⊢ ∃ r > 0, ∀ x ∈ s, 0 < r

Tactic:
⟨1, zero_lt_one, fun _ _ => zero_lt_one⟩

Premises used: zero_lt_one, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
I : Finset ι
hI : I = ∅
⊢ ∃ r > 0, ∀ x ∈ s, 0 < r

Tactic:
exact ⟨1, zero_lt_one, fun _ _ => zero_lt_one⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
G : Type u_8
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
f : G → E
s : Set G
hp : WithSeminorms p
simp_rw :
  (∀ (i : ι), ∃ r > 0, ∀ x ∈ f '' s, (p i : (a : E) → ℝ) x < r) ↔
    ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) (f x) < r
⊢ IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) (f x) < r

Tactic:
simp_rw [hp.isVonNBounded_iff_seminorm_bounded, Set.forall_mem_image]

Premises used: WithSeminorms.isVonNBounded_iff_seminorm_bounded, Set.forall_mem_image
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
simp_rw :
  (∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔
    ∀ (i : ι), ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
⊢ IsVonNBounded 𝕜 s ↔ ∀ (i : ι), BddAbove (α := ℝ) ((⇑(p i) : (a : E) → ℝ) '' s)

Tactic:
simp_rw [hp.isVonNBounded_iff_seminorm_bounded, bddAbove_def, forall_mem_image]

Premises used: bddAbove_def, WithSeminorms.isVonNBounded_iff_seminorm_bounded, Set.forall_mem_image
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
a :
  ∀ (i : ι),
    (∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔ ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
⊢ (∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔
    ∀ (i : ι), ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x

Tactic:
congrm ∀ i, ?_
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
a : (∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) → ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x
a₁ : (∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x) → ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
⊢ (∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r) ↔ ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x

Tactic:
constructor
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
r : ℝ
h_1 : r > 0 ∧ ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
h : ∀ ⦃x : E⦄, x ∈ s → (p i : (a : E) → ℝ) x ≤ r
⊢ ∃ (x : ℝ), ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i : (a : E) → ℝ) x_1 ≤ x

Tactic:
use r
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
r : ℝ
h : r > 0 ∧ ∀ x ∈ s, (p i : (a : E) → ℝ) x < r
⊢ ∀ ⦃x : E⦄, x ∈ s → (p i : (a : E) → ℝ) x ≤ r

Tactic:
grind
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
r : ℝ
h_1 : ∀ ⦃x : E⦄, x ∈ s → (p i : (a : E) → ℝ) x ≤ r
h : 1 + max r 0 > 0 ∧ ∀ x ∈ s, (p i : (a : E) → ℝ) x < 1 + max r 0
⊢ ∃ r > 0, ∀ x ∈ s, (p i : (a : E) → ℝ) x < r

Tactic:
use 1 + max r 0

Premises used: Max.max, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst_3 : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
r : ℝ
h : ∀ ⦃x : E⦄, x ∈ s → (p i : (a : E) → ℝ) x ≤ r
⊢ 1 + max r 0 > 0 ∧ ∀ x ∈ s, (p i : (a : E) → ℝ) x < 1 + max r 0

Tactic:
grind
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
⊢ (WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p) ↔
    Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1) ∧ IsVonNBounded 𝕜 (p.ball 0 1)

Tactic:
⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩

Premises used: And.intro, Iff.intro
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
refine_1 :
  ∀ (h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p),
    Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
refine_2 :
  ∀ (h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p), IsVonNBounded 𝕜 (p.ball 0 1)
refine_3 :
  Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1) ∧ IsVonNBounded 𝕜 (p.ball 0 1) →
    WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
⊢ (WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p) ↔
    Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1) ∧ IsVonNBounded 𝕜 (p.ball 0 1)

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
refine_1 : ∃ (s : Finset (Fin 1)), ∃ r > 0, ball.{u_2, u_6} (𝕜 := 𝕜) (s.sup fun (x : Fin 1) ↦ p) 0 r ⊆ p.ball 0 1
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)

Tactic:
apply (h.mem_nhds_iff _ _).2

Premises used: Iff.mpr, WithSeminorms.mem_nhds_iff
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
⊢ ball.{u_2, u_6} (𝕜 := 𝕜) (Finset.sup Finset.univ fun (x : Fin 1) ↦ p) 0 1 ⊆ p.ball 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
⊢ ∃ (s : Finset (Fin 1)), ∃ r > 0, ball.{u_2, u_6} (𝕜 := 𝕜) (s.sup fun (x : Fin 1) ↦ p) 0 r ⊆ p.ball 0 1

Tactic:
exact ⟨Finset.univ, 1, zero_lt_one, by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
apply : ∀ (i : Fin 1), ∃ r > 0, ∀ x ∈ p.ball 0 1, (p : (a : E) → ℝ) x < r
⊢ IsVonNBounded 𝕜 (p.ball 0 1)

Tactic:
apply h.isVonNBounded_iff_seminorm_bounded.2 (fun i ↦ ?_)

Premises used: Iff.mpr, WithSeminorms.isVonNBounded_iff_seminorm_bounded
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
i : Fin 1
⊢ ∀ x ∈ p.ball 0 1, LT.lt (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p
i : Fin 1
⊢ ∃ r > 0, ∀ x ∈ p.ball 0 1, (p : (a : E) → ℝ) x < r

Tactic:
exact ⟨1, zero_lt_one, by simp⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
refine_3 :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ WithSeminorms.{u_2, u_6, 0} (𝕜 := 𝕜) (E := E) (ι := Fin 1) fun (x : Fin 1) ↦ p

Tactic:
apply SeminormFamily.withSeminorms_of_nhds

Premises used: SeminormFamily.withSeminorms_of_nhds
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
refine_3 :
  ∀ (s : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) s ↔
      Membership.mem (γ := Filter E)
        (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
ext s
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
⊢ Membership.mem (γ := Filter E) (𝓝 0) s ↔
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s

Tactic:
⟨fun hs ↦ ?_, fun hs ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
refine_3 :
  ∀ (hs : Membership.mem (γ := Filter E) (𝓝 0) s),
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s
refine_3₁ :
  ∀
    (hs :
      Membership.mem (γ := Filter E)
        (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s),
    Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Membership.mem (γ := Filter E) (𝓝 0) s ↔
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s

Tactic:
refine ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
⊢ ∃ (c : 𝕜), p.ball 0 1 ⊆ c • s ∧ c ≠ 0

Tactic:
((h' hs).and (eventually_ne_cobounded 0)).exists

Premises used: Bornology.eventually_ne_cobounded, Filter.Eventually.and, Filter.Eventually.exists, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
refine_3 :
  ∀ (c : 𝕜) (hc : p.ball 0 1 ⊆ c • s) (c_ne : c ≠ 0),
    Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
      s
⊢ Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s

Tactic:
obtain ⟨c, hc, c_ne⟩ : ∃ (c : 𝕜), p.ball 0 1 ⊆ c • s ∧ c ≠ 0 :=
      ((h' hs).and (eventually_ne_cobounded 0)).exists

Premises used: Bornology.eventually_ne_cobounded, Filter.Eventually.and, Filter.Eventually.exists, Seminorm.ball, OfNat.ofNat
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
⊢ c • p.ball 0 ‖c⁻¹‖ ⊆ c • s

Tactic:
simpa [smul_ball_zero c_ne, ← norm_mul, c_ne] using hc

Premises used: norm_mul, Seminorm.smul_ball_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
⊢ c • p.ball 0 ‖c⁻¹‖ ⊆ c • s

Tactic:
have : c • p.ball 0 (‖c⁻¹‖) ⊆ c • s := by
        simpa [smul_ball_zero c_ne, ← norm_mul, c_ne] using hc
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : c • p.ball 0 ‖c⁻¹‖ ⊆ c • s
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : p.ball 0 ‖c⁻¹‖ ⊆ s), p.ball 0 ‖c⁻¹‖ ⊆ s
⊢ p.ball 0 ‖c⁻¹‖ ⊆ s

Tactic:
rwa [smul_set_subset_smul_set_iff₀ c_ne] at this

Premises used: Set.smul_set_subset_smul_set_iff₀
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
⊢ p.ball 0 ‖c⁻¹‖ ⊆ s

Tactic:
have : p.ball 0 (‖c⁻¹‖) ⊆ s := by
      have : c • p.ball 0 (‖c⁻¹‖) ⊆ c • s := by
        simpa [smul_ball_zero c_ne, ← norm_mul, c_ne] using hc
      rwa [smul_set_subset_smul_set_iff₀ c_ne] at this
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
refine_3 :
  Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (p.ball 0 ‖c⁻¹‖)
⊢ Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s

Tactic:
grw [← this]
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
refine_3 :
  Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) (p.ball 0 ‖c⁻¹‖)
⊢ Membership.mem (γ := Filter E) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
    (p.ball 0 ‖c⁻¹‖)

Tactic:
apply FilterBasis.mem_filter_of_mem

Premises used: FilterBasis.mem_filter_of_mem
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
h : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 1)
h' : IsVonNBounded 𝕜 (p.ball 0 1)
s : Set E
hs : Membership.mem (γ := Filter E) (𝓝 0) s
c : 𝕜
hc : p.ball 0 1 ⊆ c • s
c_ne : c ≠ 0
this : p.ball 0 ‖c⁻¹‖ ⊆ s
refine_3 : 0 < ‖c⁻¹‖
⊢ Membership.mem (γ := Set (Set E)) (SeminormFamily.basisSets.{u_2, u_6, 0} (R := 𝕜) (ι := Fin 1) fun (i : Fin 1) ↦ p)
    (p.ball 0 ‖c⁻¹‖)

Tactic:
apply SeminormFamily.basisSets_singleton_mem _ 0

Premises used: SeminormFamily.basisSets_singleton_mem, OfNat.ofNat