awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 0 < ‖c⁻¹‖

Tactic:
simpa using c_ne
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
refine_3 :
  ∀ (t : Set E)
    (ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t)
    (ts : t ⊆ s), Membership.mem (γ := Filter E) (𝓝 0) s
⊢ Membership.mem (γ := Filter E) (𝓝 0) s

Tactic:
rcases (FilterBasis.mem_filter_iff _).1 hs with ⟨t, ht, ts⟩

Premises used: FilterBasis.mem_filter_iff, Iff.mp
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
refine_3 : Membership.mem (γ := Filter E) (𝓝 0) t
⊢ Membership.mem (γ := Filter E) (𝓝 0) s

Tactic:
grw [← ts]
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
refine_3 :
  ∀ (w : Finset (Fin 1)) (r : ℝ) (r_pos : 0 < r) (hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r),
    Membership.mem (γ := Filter E) (𝓝 0) t
⊢ Membership.mem (γ := Filter E) (𝓝 0) t

Tactic:
rcases (SeminormFamily.basisSets_iff _).1 ht with ⟨w, r, r_pos, hw⟩

Premises used: Iff.mp, SeminormFamily.basisSets_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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
refine_3 :
  ∀ (hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (Finset.sup ∅ fun (x : Fin 1) ↦ p) 0 r), Membership.mem (γ := Filter E) (𝓝 0) t
refine_3₁ : ∀ (w_ne : w ≠ ∅), Membership.mem (γ := Filter E) (𝓝 0) t
⊢ Membership.mem (γ := Filter E) (𝓝 0) t

Tactic:
rcases eq_or_ne w ∅ with rfl | w_ne

Premises used: eq_or_ne, EmptyCollection.emptyCollection, rfl
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (Finset.sup ∅ fun (x : Fin 1) ↦ p) 0 r
⊢ t = univ

Tactic:
simp only [ball, Finset.sup_empty, sub_zero, coe_bot, Pi.zero_apply, r_pos, setOf_true] at hw

Premises used: sub_zero, Pi.zero_apply, Finset.sup_empty, Seminorm.coe_bot, Seminorm.ball, Set.setOf_true
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
r : ℝ
r_pos : 0 < r
hw : t = univ
⊢ Membership.mem (γ := Filter E) (𝓝 0) t

Tactic:
simp [hw]
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
rcases : ∀ (i : Fin 1) (hi : i ∈ w), w = Finset.univ
⊢ w = Finset.univ

Tactic:
rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩

Premises used: Finset.nonempty_of_ne_empty
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
i : Fin 1
hi : i ∈ w
h₁ : ∀ (j : Fin 1), j ∈ w ↔ Membership.mem (γ := Finset (Fin 1)) Finset.univ j
⊢ w = Finset.univ

Tactic:
ext j
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
i : Fin 1
hi : i ∈ w
j : Fin 1
⊢ j ∈ w ↔ Membership.mem (γ := Finset (Fin 1)) Finset.univ j

Tactic:
simp only [Subsingleton.elim j i, hi, Finset.mem_univ]

Premises used: Finset.mem_univ, Subsingleton.elim
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
⊢ w = Finset.univ

Tactic:
have : w = Finset.univ := by
        rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩
        ext j
        simp only [Subsingleton.elim j i, hi, Finset.mem_univ]
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : w = Finset.univ
⊢ t = p.ball 0 r

Tactic:
simpa only [this, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
        Finset.sup_singleton] using hw

Premises used: Finset.sup_singleton, Finset.univ_unique, Fin.isValue, Fin.default_eq_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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
⊢ t = p.ball 0 r

Tactic:
have : t = p.ball 0 r := by
      have : w = Finset.univ := by
        rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩
        ext j
        simp only [Subsingleton.elim j i, hi, Finset.mem_univ]
      simpa only [this, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
        Finset.sup_singleton] using hw
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
refine_3 : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
⊢ Membership.mem (γ := Filter E) (𝓝 0) t

Tactic:
rw [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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
⊢ ∃ (c : 𝕜), 0 < ‖c‖ ∧ ‖c‖ < r

Tactic:
exists_norm_lt 𝕜 r_pos

Premises used: NormedField.exists_norm_lt
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
refine_3 : ∀ (c : 𝕜) (c_pos : 0 < ‖c‖) (hc : ‖c‖ < r), Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)

Tactic:
obtain ⟨c, c_pos, hc⟩ : ∃ (c : 𝕜), 0 < ‖c‖ ∧ ‖c‖ < r := exists_norm_lt 𝕜 r_pos

Premises used: NormedField.exists_norm_lt
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
⊢ c ≠ 0

Tactic:
simpa using c_pos
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
⊢ c ≠ 0

Tactic:
have c_ne : c ≠ 0 := (by simpa using c_pos)
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
rw : p.ball 0 (‖c‖ * 1) ⊆ p.ball 0 r
⊢ c • p.ball 0 1 ⊆ p.ball 0 r

Tactic:
rw [smul_ball_zero c_ne]

Premises used: 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
⊢ ‖c‖ * 1 ≤ r

Tactic:
simpa using hc.le

Premises used: LT.lt.le
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
⊢ p.ball 0 (‖c‖ * 1) ⊆ p.ball 0 r

Tactic:
exact ball_mono (by simpa using hc.le)

Premises used: Seminorm.ball_mono
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
⊢ c • p.ball 0 1 ⊆ p.ball 0 r

Tactic:
have : c • p.ball 0 1 ⊆ p.ball 0 r := by
      rw [smul_ball_zero c_ne]
      exact ball_mono (by simpa using hc.le)
-- 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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this_1 : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
this : c • p.ball 0 1 ⊆ p.ball 0 r
refine_3 : Membership.mem (γ := Filter E) (𝓝 0) (c • p.ball 0 1)
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)

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) (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _)) s
t : Set E
ht : Membership.mem (γ := FilterBasis E) (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _) t
ts : t ⊆ s
w : Finset (Fin 1)
r : ℝ
r_pos : 0 < r
hw : t = ball.{u_2, u_6} (𝕜 := 𝕜) (w.sup fun (x : Fin 1) ↦ p) 0 r
w_ne : w ≠ ∅
this_1 : t = p.ball 0 r
c : 𝕜
c_pos : 0 < ‖c‖
hc : ‖c‖ < r
c_ne : c ≠ 0
this : c • p.ball 0 1 ⊆ p.ball 0 r
⊢ Membership.mem (γ := Filter E) (𝓝 0) (c • p.ball 0 1)

Tactic:
simpa using smul_mem_nhds_smul₀ c_ne h

Premises used: smul_mem_nhds_smul₀
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
⊢ IsTopologicalAddGroup F

Tactic:
have : IsTopologicalAddGroup F := hq.topologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
⊢ Continuous[inst_7, inst_9] (⇑f : (a : E) → F)

Tactic:
continuous_of_continuousAt_zero f ?_

Premises used: continuous_of_continuousAt_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕝 : Type u_4
𝕝₂ : Type u_5
E : Type u_6
F : Type u_7
ι' : Type u_10
inst : AddCommGroup E
inst_1 : NormedField 𝕝
inst_2 : Module 𝕝 E
inst_3 : AddCommGroup F
inst_4 : NormedField 𝕝₂
inst_5 : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst_6 : RingHomIsometric τ₁₂
q : SeminormFamily 𝕝₂ F ι'
inst_7 : TopologicalSpace E
inst_8 : IsTopologicalAddGroup E
inst_9 : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : ∀ (i : ι'), Continuous[inst_7, _] (⇑((q i).comp f) : (a : E) → ℝ)
this : IsTopologicalAddGroup F
refine : ContinuousAt.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F) 0
⊢ Continuous[inst_7, inst_9] (⇑f : (a : E) → F)

Tactic:
refine continuous_of_continuousAt_zero f ?_

Premises used: continuous_of_continuousAt_zero