awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
by_contra! : ∀ (h : ∀ (i : ι), Eq (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)), False
⊢ ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), Eq (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ False

Tactic:
hx (this ?_)
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), Eq (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
refine : x ⤳ 0
⊢ False

Tactic:
refine hx (this ?_)
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), Eq (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
rw : ∀ (i : Finset ι × ℝ), 0 < i.2 → x ∈ (i.1.sup p).ball 0 i.2
⊢ x ⤳ 0

Tactic:
rw [hp.hasBasis_zero_ball.specializes_iff]

Premises used: Filter.HasBasis.specializes_iff, WithSeminorms.hasBasis_zero_ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), Eq (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ x ∈ ((s, r).1.sup p).ball 0 (s, r).2

Tactic:
simp only [ball_finset_sup_eq_iInter _ _ _ hr, mem_iInter₂, mem_ball_zero, h, hr, forall_true_iff]

Premises used: Seminorm.mem_ball_zero, Set.mem_iInter₂, forall_true_iff, Seminorm.ball_finset_sup_eq_iInter
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)) ↔ T1Space E

Tactic:
⟨WithSeminorms.T1_of_separating hp, ?_⟩

Premises used: WithSeminorms.T1_of_separating, Iff.intro
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
refine : T1Space E → ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ (∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)) ↔ T1Space E

Tactic:
refine ⟨WithSeminorms.T1_of_separating hp, ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : T1Space E
⊢ ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
WithSeminorms.separating_of_T1 hp

Premises used: WithSeminorms.separating_of_T1
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
h : T1Space E
⊢ ∀ (x : E), x ≠ 0 → ∃ (i : ι), Ne (α := ℝ) ((p i : (a : E) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
exact WithSeminorms.separating_of_T1 hp

Premises used: WithSeminorms.separating_of_T1
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ Tendsto u f (𝓝 y₀) ↔ ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p : (a : E) → ℝ) (u x - y₀) < ε

Tactic:
simp [hp.hasBasis_ball.tendsto_right_iff]

Premises used: Filter.HasBasis.tendsto_right_iff, WithSeminorms.hasBasis_ball
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
rw :
  (∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p : (a : E) → ℝ) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i : (a : E) → ℝ) (u x - y₀) < ε
⊢ Tendsto u f (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i : (a : E) → ℝ) (u x - y₀) < ε

Tactic:
rw [hp.tendsto_nhds' u y₀]

Premises used: WithSeminorms.tendsto_nhds'
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
h : ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p : (a : E) → ℝ) (u x - y₀) < ε
i : ι
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i : (a : E) → ℝ) (u x - y₀) < ε

Tactic:
simpa only [Finset.sup_singleton] using h {i}

Premises used: Finset.sup_singleton, Singleton.singleton
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ (∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p : (a : E) → ℝ) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i : (a : E) → ℝ) (u x - y₀) < ε

Tactic:
exact
    ⟨fun h i => by simpa only [Finset.sup_singleton] using h {i}, fun h s ε hε =>
      (s.eventually_all.2 fun i _ => h i ε hε).mono fun _ => finset_sup_apply_lt hε⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : SemilatticeSup F
inst_5 : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
rw :
  (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i : (a : E) → ℝ) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ (x₀ : F), ∀ (x : F), x₀ ≤ x → (p i : (a : E) → ℝ) (u x - y₀) < ε
⊢ Tendsto u atTop (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ (x₀ : F), ∀ (x : F), x₀ ≤ x → (p i : (a : E) → ℝ) (u x - y₀) < ε

Tactic:
rw [hp.tendsto_nhds u y₀]

Premises used: WithSeminorms.tendsto_nhds
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : SemilatticeSup F
inst_5 : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i : (a : E) → ℝ) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ (x₀ : F), ∀ (x : F), x₀ ≤ x → (p i : (a : E) → ℝ) (u x - y₀) < ε

Tactic:
forall₃_congr fun _ _ _ => Filter.eventually_atTop

Premises used: forall₃_congr, Filter.eventually_atTop
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst_4 : SemilatticeSup F
inst_5 : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i : (a : E) → ℝ) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ (x₀ : F), ∀ (x : F), x₀ ≤ x → (p i : (a : E) → ℝ) (u x - y₀) < ε

Tactic:
exact forall₃_congr fun _ _ _ => Filter.eventually_atTop

Premises used: forall₃_congr, Filter.eventually_atTop
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ WithSeminorms p

Tactic:
⟨IsTopologicalAddGroup.ext inferInstance p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩

Premises used: WithSeminorms.mk, AddGroupFilterBasis.isTopologicalAddGroup, inferInstance, IsTopologicalAddGroup.ext, SeminormFamily.addGroupFilterBasis
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
inferInstance : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
⊢ WithSeminorms p

Tactic:
refine
    ⟨IsTopologicalAddGroup.ext inferInstance p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
rw :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (𝓝 0)

Tactic:
rw [AddGroupFilterBasis.nhds_zero_eq]

Premises used: AddGroupFilterBasis.nhds_zero_eq
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
h
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
exact h
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : HasBasis (𝓝 0) (fun (s : Set E) ↦ s ∈ p.basisSets) id
⊢ WithSeminorms p

Tactic:
p.withSeminorms_of_nhds <|
    Filter.HasBasis.eq_of_same_basis h p.addGroupFilterBasis.toFilterBasis.hasBasis

Premises used: AddGroupFilterBasis.toFilterBasis, FilterBasis.hasBasis, SeminormFamily.withSeminorms_of_nhds, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
rw :
  WithSeminorms p ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
      (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ WithSeminorms p ↔ Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))

Tactic:
rw [← p.filter_eq_iInf]

Premises used: SeminormFamily.filter_eq_iInf
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
      (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
⟨fun h => ?_, p.withSeminorms_of_nhds⟩

Premises used: Iff.intro, SeminormFamily.withSeminorms_of_nhds
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
refine :
  ∀ (h : WithSeminorms p),
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
      (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ WithSeminorms p ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
      (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
refine ⟨fun h => ?_, p.withSeminorms_of_nhds⟩
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
rw :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
rw [h.topology_eq_withSeminorms]

Premises used: WithSeminorms.topology_eq_withSeminorms
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
AddGroupFilterBasis.nhds_zero_eq _

Premises used: AddGroupFilterBasis.nhds_zero_eq
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
h : WithSeminorms p
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (FilterBasis.filter (@AddGroupFilterBasis.toFilterBasis _ AddCommGroup.toAddGroup _))

Tactic:
exact AddGroupFilterBasis.nhds_zero_eq _

Premises used: AddGroupFilterBasis.nhds_zero_eq
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
rw :
  Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), 𝓝 0)
⊢ WithSeminorms p ↔ t = ⨅ (i : ι), UniformSpace.toTopologicalSpace

Tactic:
rw [p.withSeminorms_iff_nhds_eq_iInf,
    IsTopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_iInf fun i => inferInstance),
    nhds_iInf]

Premises used: nhds_iInf, IsTopologicalAddGroup.ext_iff, inferInstance, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, topologicalAddGroup_iInf
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
a : ∀ (i : ι), Eq (α := Filter E) (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) (𝓝 0)
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) ↔
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), 𝓝 0)

Tactic:
congrm _ = ⨅ i, ?_
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ Eq (α := Filter E) (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) (𝓝 0)

Tactic:
@comap_norm_nhds_zero _ (p i).toSeminormedAddGroup

Premises used: comap_norm_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ Eq (α := Filter E) (comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)) (𝓝 0)

Tactic:
exact @comap_norm_nhds_zero _ (p i).toSeminormedAddGroup

Premises used: comap_norm_nhds_zero
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
⊢ IsTopologicalAddGroup E

Tactic:
have := hp.topologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
this : IsTopologicalAddGroup E
rw : Continuous[⨅ (i : ι), PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑(p i) : (a : E) → ℝ)
⊢ Continuous[t, _] (⇑(p i) : (a : E) → ℝ)

Tactic:
rw [p.withSeminorms_iff_topologicalSpace_eq_iInf.mp hp]

Premises used: SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf, Iff.mp
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
this : IsTopologicalAddGroup E
⊢ Continuous[⨅ (i : ι), PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑(p i) : (a : E) → ℝ)

Tactic:
continuous_iInf_dom (@continuous_norm _ (p i).toSeminormedAddGroup)

Premises used: continuous_iInf_dom, continuous_norm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
this : IsTopologicalAddGroup E
⊢ Continuous[⨅ (i : ι), PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑(p i) : (a : E) → ℝ)

Tactic:
exact continuous_iInf_dom (@continuous_norm _ (p i).toSeminormedAddGroup)

Premises used: continuous_iInf_dom
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ IsTopologicalAddGroup E

Tactic:
have := hp.topologicalAddGroup
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
⊢ ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)

Tactic:
have hp' (i : ι) : Continuous (p i) := hp.continuous_seminorm i
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
rw :
  ∀ (hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0)))
    (this : IsTopologicalAddGroup E) (hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)),
    Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
      (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
        comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
⊢ WithSeminorms.{u_2, u_6, u_6} (𝕜 := 𝕜) (E := E) (ι := { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) })
    fun (p : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }) ↦ (↑p : Seminorm 𝕜 E)

Tactic:
rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf] at ⊢ hp

Premises used: SeminormFamily.withSeminorms_iff_nhds_eq_iInf
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
refine_1 :
  LE.le.{u_6} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
refine_2 :
  LE.le.{u_6} (α := Filter E)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))
    (𝓝 0)
⊢ Eq.{u_6 + 1} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p i) : (a : E) → ℝ)
refine_1 :
  ∀ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
    Tendsto (α := E) (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0) (𝓝 0)
⊢ LE.le.{u_6} (α := Filter E) (𝓝 0)
    (⨅ (i : { p : Seminorm 𝕜 E // Continuous[t, _] (⇑p : (a : E) → ℝ) }),
      comap (β := ℝ) (⇑(↑i : Seminorm 𝕜 E) : (a : E) → ℝ) (𝓝 0))

Tactic:
simp_rw [le_iInf_iff, ← tendsto_iff_comap]

Premises used: le_iInf_iff, Filter.tendsto_iff_comap
-- Module: Mathlib.Analysis.LocallyConvex.WithSeminorms
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t : TopologicalSpace E
p_1 : SeminormFamily 𝕜 E ι
hp_1 : Eq.{u_6 + 1} (α := Filter E) (𝓝 0) (⨅ (i : ι), comap (β := ℝ) (⇑(p_1 i) : (a : E) → ℝ) (𝓝 0))
this : IsTopologicalAddGroup E
hp' : ∀ (i : ι), Continuous[t, _] (⇑(p_1 i) : (a : E) → ℝ)
p : Seminorm 𝕜 E
hp : Continuous[t, _] (⇑p : (a : E) → ℝ)
⊢ Tendsto (α := E) (β := ℝ)
    (⇑(↑(Subtype.mk (p := fun (p : Seminorm 𝕜 E) ↦ Continuous[t, _] (⇑p : (a : E) → ℝ)) p hp) : Seminorm 𝕜 E) :
      (a : E) → ℝ)
    (𝓝 0) (𝓝 0)

Tactic:
hp.tendsto' 0 0 (map_zero _)

Premises used: map_zero, Continuous.tendsto', OfNat.ofNat