awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
⊢ Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)

Tactic:
have hp : Filter.Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp_1 : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
hp : Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)
rw :
  Tendsto.{u_7, 0} (α := E × E) (β := ℝ)
    ((fun (p : ℝ × ℝ) ↦ dist p.1 p.2) ∘ fun (x : E × E) ↦ ((p : (a : E) → ℝ) x.1, (p : (a : E) → ℝ) x.2))
    (comap (β := E) (fun (x : E × E) ↦ x.1 - x.2) (𝓝 0)) (𝓝 0)
⊢ UniformContinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)

Tactic:
rw [UniformContinuous, uniformity_eq_comap_nhds_zero_swapped,
    Metric.uniformity_eq_comap_nhds_zero, Filter.tendsto_comap_iff]

Premises used: UniformContinuous, Filter.tendsto_comap_iff, uniformity_eq_comap_nhds_zero_swapped, Metric.uniformity_eq_comap_nhds_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp_1 : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
hp : Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)
⊢ Tendsto.{u_7, 0} (α := E × E) (β := ℝ)
    ((fun (p : ℝ × ℝ) ↦ dist p.1 p.2) ∘ fun (x : E × E) ↦ ((p : (a : E) → ℝ) x.1, (p : (a : E) → ℝ) x.2))
    (comap (β := E) (fun (x : E × E) ↦ x.1 - x.2) (𝓝 0)) (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hp.comp Filter.tendsto_comap)
      (fun xy => dist_nonneg) fun xy => p.norm_sub_map_le_sub _ _

Premises used: Seminorm.norm_sub_map_le_sub, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, dist_nonneg, Filter.tendsto_comap, Prod.fst, Filter.Tendsto.comp, Prod.snd
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp_1 : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
hp : Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)
⊢ Tendsto.{u_7, 0} (α := E × E) (β := ℝ)
    ((fun (p : ℝ × ℝ) ↦ dist p.1 p.2) ∘ fun (x : E × E) ↦ ((p : (a : E) → ℝ) x.1, (p : (a : E) → ℝ) x.2))
    (comap (β := E) (fun (x : E × E) ↦ x.1 - x.2) (𝓝 0)) (𝓝 0)

Tactic:
exact
    tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hp.comp Filter.tendsto_comap)
      (fun xy => dist_nonneg) fun xy => p.norm_sub_map_le_sub _ _

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, dist_nonneg, Filter.tendsto_comap, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
this : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ IsUniformAddGroup E

Tactic:
haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
(Seminorm.uniformContinuous_of_continuousAt_zero hp).continuous

Premises used: Seminorm.uniformContinuous_of_continuousAt_zero, UniformContinuous.continuous
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ContinuousAt (X := E) (Y := ℝ) (⇑p : (a : E) → ℝ) 0
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
exact (Seminorm.uniformContinuous_of_continuousAt_zero hp).continuous

Premises used: Seminorm.uniformContinuous_of_continuousAt_zero, UniformContinuous.continuous
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp : ∀ r > 0, Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
⊢ UniformContinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero_of_forall hp)

Premises used: Seminorm.uniformContinuous_of_continuousAt_zero, Seminorm.continuousAt_zero_of_forall
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
⊢ UniformContinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero hp)

Premises used: Seminorm.uniformContinuous_of_continuousAt_zero, Seminorm.continuousAt_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
p : Seminorm 𝕝 E
hp : ∀ r > 0, Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
⊢ UniformContinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero_of_forall' hp)

Premises used: Seminorm.continuousAt_zero_of_forall', Seminorm.uniformContinuous_of_continuousAt_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
⊢ UniformContinuous (α := E) (β := ℝ) (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.uniformContinuous_of_continuousAt_zero (continuousAt_zero' hp)

Premises used: Seminorm.uniformContinuous_of_continuousAt_zero, Seminorm.continuousAt_zero'
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ∀ r > 0, Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.continuous_of_continuousAt_zero (continuousAt_zero_of_forall hp)

Premises used: Seminorm.continuousAt_zero_of_forall, Seminorm.continuous_of_continuousAt_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
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
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.continuous_of_continuousAt_zero (continuousAt_zero hp)

Premises used: Seminorm.continuous_of_continuousAt_zero, Seminorm.continuousAt_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
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
r : ℝ
hr : 0 < r
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ) ↔ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)

Tactic:
⟨fun H ↦ p.ball_zero_eq ▸ (H.tendsto' 0 0 (map_zero p)).eventually_lt_const hr, p.continuous⟩

Premises used: Seminorm.continuous, Eq.rec, map_zero, Filter.Tendsto.eventually_lt_const, Iff.intro, Continuous.tendsto', OfNat.ofNat, Eq.symm, Seminorm.ball_zero_eq
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p : Seminorm 𝕝 E
hp : ∀ r > 0, Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.continuous_of_continuousAt_zero (continuousAt_zero_of_forall' hp)

Premises used: Seminorm.continuousAt_zero_of_forall', Seminorm.continuous_of_continuousAt_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
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
r : ℝ
hp : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.continuous_of_continuousAt_zero (continuousAt_zero' hp)

Premises used: Seminorm.continuousAt_zero', Seminorm.continuous_of_continuousAt_zero
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst_3, _] (⇑q : (a : E) → ℝ)
hpq : p ≤ q
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
Seminorm.continuous_of_forall (fun r hr ↦ Filter.mem_of_superset
    (IsOpen.mem_nhds ?_ <| q.mem_ball_self hr) (ball_antitone hpq))

Premises used: Seminorm.ball_antitone, Seminorm.mem_ball_self, IsOpen.mem_nhds, Seminorm.continuous_of_forall, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst_3, _] (⇑q : (a : E) → ℝ)
hpq : p ≤ q
refine : ∀ (r : ℝ) (hr : r > 0), IsOpen[inst_3] (q.ball 0 r)
⊢ Continuous[inst_3, _] (⇑p : (a : E) → ℝ)

Tactic:
refine Seminorm.continuous_of_forall (fun r hr ↦ Filter.mem_of_superset
    (IsOpen.mem_nhds ?_ <| q.mem_ball_self hr) (ball_antitone hpq))

Premises used: Seminorm.ball_antitone, Seminorm.mem_ball_self, IsOpen.mem_nhds, Seminorm.continuous_of_forall, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst_3, _] (⇑q : (a : E) → ℝ)
hpq : p ≤ q
r : ℝ
hr : r > 0
rw : IsOpen[inst_3] {y : E | (q : (a : E) → ℝ) y < r}
⊢ IsOpen[inst_3] (q.ball 0 r)

Tactic:
rw [ball_zero_eq]

Premises used: Seminorm.ball_zero_eq
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst_3, _] (⇑q : (a : E) → ℝ)
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen[inst_3] {y : E | (q : (a : E) → ℝ) y < r}

Tactic:
isOpen_lt hq continuous_const

Premises used: isOpen_lt, continuous_const, setOf
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
inst_4 : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous[inst_3, _] (⇑q : (a : E) → ℝ)
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen[inst_3] {y : E | (q : (a : E) → ℝ) y < r}

Tactic:
exact isOpen_lt hq continuous_const

Premises used: isOpen_lt, continuous_const
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
p : Seminorm 𝕝 E
hp : Continuous[inst_3, _] (⇑p : (a : E) → ℝ)
r : ℝ
hr : 0 < r
⊢ Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)

Tactic:
have this : Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp.tendsto 0
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕝 : Type u_6
E : Type u_7
inst : SeminormedRing 𝕝
inst_1 : AddCommGroup E
inst_2 : Module 𝕝 E
inst_3 : TopologicalSpace E
p : Seminorm 𝕝 E
hp : Continuous[inst_3, _] (⇑p : (a : E) → ℝ)
r : ℝ
hr : 0 < r
this : Tendsto (α := E) (β := ℝ) (⇑p : (a : E) → ℝ) (𝓝 0) (𝓝 0)
⊢ Membership.mem (γ := Filter E) (𝓝 0) (p.ball 0 r)

Tactic:
simpa only [p.ball_zero_eq] using this (Iio_mem_nhds hr)

Premises used: Iio_mem_nhds, Seminorm.ball_zero_eq
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ inst_3 = PseudoMetricSpace.toUniformSpace

Tactic:
IsUniformAddGroup.ext ‹_›
    p.toAddGroupSeminorm.toSeminormedAddCommGroup.to_isUniformAddGroup ?_

Premises used: IsUniformAddGroup.ext, SeminormedAddCommGroup.to_isUniformAddGroup
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
refine : Eq.{u_7 + 1} (α := Filter E) (𝓝 0) (𝓝 0)
⊢ inst_3 = PseudoMetricSpace.toUniformSpace

Tactic:
refine IsUniformAddGroup.ext ‹_›
    p.toAddGroupSeminorm.toSeminormedAddCommGroup.to_isUniformAddGroup ?_

Premises used: IsUniformAddGroup.ext, SeminormedAddCommGroup.to_isUniformAddGroup
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
a : LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)
a₁ : LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)
⊢ Eq.{u_7 + 1} (α := Filter E) (𝓝 0) (𝓝 0)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
a : Tendsto.{u_7, 0} (α := E) norm (𝓝 0) (𝓝 0)
⊢ LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)

Tactic:
rw [← @comap_norm_nhds_zero E p.toAddGroupSeminorm.toSeminormedAddGroup, ← tendsto_iff_comap]

Premises used: comap_norm_nhds_zero, Filter.tendsto_iff_comap
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
a : Continuous[inst_3.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
⊢ Tendsto.{u_7, 0} (α := E) norm (𝓝 0) (𝓝 0)

Tactic:
suffices Continuous p from this.tendsto' 0 _ (map_zero p)
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
a :
  ∀ (r : ℝ) (hr : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)),
    Continuous[inst_3.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)
⊢ Continuous[inst_3.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)

Tactic:
rcases h₁ with ⟨r, hr⟩
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
r : ℝ
hr : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
⊢ Continuous[inst_3.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)

Tactic:
p.continuous' hr

Premises used: Seminorm.continuous'
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
r : ℝ
hr : Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
⊢ Continuous[inst_3.toTopologicalSpace, _] (⇑p : (a : E) → ℝ)

Tactic:
exact p.continuous' hr

Premises used: Seminorm.continuous'
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
a : ∀ (i' : ι), p' i' → ∃ (i : ℝ), 0 < i ∧ {y : E | ‖y‖ < i} ⊆ s i'
⊢ LE.le.{u_7} (α := Filter E) (𝓝 0) (𝓝 0)

Tactic:
rw [(@NormedAddGroup.nhds_zero_basis_norm_lt E
      p.toAddGroupSeminorm.toSeminormedAddGroup).le_basis_iff hb]

Premises used: Filter.HasBasis.le_basis_iff, NormedAddGroup.nhds_zero_basis_norm_lt
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ ∀ (i' : ι), p' i' → ∃ (i : ℝ), 0 < i ∧ {y : E | ‖y‖ < i} ⊆ s i'

Tactic:
simpa only [subset_def, mem_ball_zero] using h₂

Premises used: Seminorm.mem_ball_zero, Set.subset_def
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
rw : 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (x.1 - x.2) < r}
⊢ 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (x.1 - x.2) < r}

Tactic:
rw [uniformSpace_eq_of_hasBasis p hb h₁ h₂]

Premises used: Seminorm.uniformSpace_eq_of_hasBasis
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
simp : 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (-x.1 + x.2) < r}
⊢ 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (x.1 - x.2) < r}

Tactic:
simp only [sub_eq_add_neg, ← map_neg_add p]

Premises used: sub_eq_add_neg, map_neg_add
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ι : Sort u_12
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : ContinuousConstSMul 𝕜 E
p' : ι → Prop
s : ι → Set E
p : Seminorm 𝕜 E
hb : HasBasis (𝓝 0) p' s
h₁ : ∃ (r : ℝ), Membership.mem (γ := Filter E) (𝓝 0) (p.closedBall 0 r)
h₂ : ∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i
⊢ 𝓤 E = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {x : E × E | (p : (a : E) → ℝ) (-x.1 + x.2) < r}

Tactic:
rfl
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
positivity
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
⊢ 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε

Tactic:
have xεpos : 0 < (p x) / ε := by positivity
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
rcases :
  ∀ (n : ℤ) (hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))),
    ∃ (n : ℤ),
      c ^ n ≠ 0 ∧
        (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
          ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)
⊢ ∃ (n : ℤ),
    c ^ n ≠ 0 ∧
      (p : (a : E) → ℝ) (c ^ n • x) < ε ∧
        ε / ‖c‖ ≤ (p : (a : E) → ℝ) (c ^ n • x) ∧ ‖c ^ n‖⁻¹ ≤ HMul.hMul (β := ℝ) (ε⁻¹ * ‖c‖) ((p : (a : E) → ℝ) x : ℝ)

Tactic:
rcases exists_mem_Ico_zpow xεpos hc with ⟨n, hn⟩

Premises used: exists_mem_Ico_zpow
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
⊢ 0 < ‖c‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
⊢ 0 < ‖c‖

Tactic:
have cpos : 0 < ‖c‖ := by positivity
-- Module: Mathlib.Analysis.Seminorm
Goal:
𝕜 : Type u_3
E : Type u_7
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : Ne (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) (0 : ℝ)
xεpos : 0 < HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε
n : ℤ
hn : HDiv.hDiv (α := ℝ) ((p : (a : E) → ℝ) x : ℝ) ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
rw : 0 < ‖c‖ ^ (n + 1)
⊢ 0 < ‖c ^ (n + 1)‖

Tactic:
rw [norm_zpow]

Premises used: norm_zpow