awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
x : E
rw : Membership.mem (γ := Set E) (closedBall 1 0) x ↔ ‖x‖ = 0
rw₁ : ‖x‖ ≤ 0 ↔ ‖x‖ = 0
rw₂ rw₃ : ‖x‖ = 0 ↔ ‖x‖ = 0
⊢ Membership.mem (γ := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {1}) x ↔ ‖x‖ = 0

Tactic:
rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).ge_iff_eq']

Premises used: norm_nonneg', Metric.closedBall_zero', LE.le.ge_iff_eq', mem_closedBall_one_iff
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
⊢ Eq (α := Set E) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {1}) {x : E | ‖x‖ = 0}

Tactic:
Set.ext fun _x => mem_closure_one_iff_norm

Premises used: Set.ext, mem_closure_one_iff_norm
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
a : E
l : Filter α
f : α → E
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ ‖f x‖) l (𝓝 ‖a‖)

Tactic:
tendsto_norm'.comp h

Premises used: tendsto_norm', Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
a : E
l : Filter α
f : α → E
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ ‖f x‖₊) l (𝓝 ‖a‖₊)

Tactic:
Tendsto.comp continuous_nnnorm'.continuousAt h

Premises used: Continuous.continuousAt, Filter.Tendsto.comp, continuous_nnnorm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
⊢ Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f → Continuous[inst_1, _] fun (x : α) ↦ ‖f x‖

Tactic:
continuous_norm'.comp

Premises used: Continuous.comp, continuous_norm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
⊢ Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f → Continuous[inst_1, _] fun (x : α) ↦ ‖f x‖₊

Tactic:
continuous_nnnorm'.comp

Premises used: Continuous.comp, continuous_nnnorm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : TopologicalSpace E
inst_1 : ContinuousENorm E
a : E
l : Filter α
f : α → E
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun (x : α) ↦ ‖f x‖ₑ) l (𝓝 ‖a‖ₑ)

Tactic:
.comp continuous_enorm.continuousAt h

Premises used: continuous_enorm, Continuous.continuousAt, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
a : α
h : ContinuousAt f a
⊢ ContinuousAt (Y := ℝ) (fun (x : α) ↦ ‖f x‖) a

Tactic:
Tendsto.norm' h

Premises used: ContinuousAt, Filter.Tendsto.norm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
a : α
h : ContinuousAt f a
⊢ ContinuousAt (Y := ℝ≥0) (fun (x : α) ↦ ‖f x‖₊) a

Tactic:
Tendsto.nnnorm' h

Premises used: ContinuousAt, Filter.Tendsto.nnnorm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
s : Set α
a : α
h : ContinuousWithinAt f s a
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : α) ↦ ‖f x‖) s a

Tactic:
Tendsto.norm' h

Premises used: ContinuousWithinAt, Filter.Tendsto.norm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
s : Set α
a : α
h : ContinuousWithinAt f s a
⊢ ContinuousWithinAt (Y := ℝ≥0) (fun (x : α) ↦ ‖f x‖₊) s a

Tactic:
Tendsto.nnnorm' h

Premises used: ContinuousWithinAt, Filter.Tendsto.nnnorm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
s : Set α
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ) (fun (x : α) ↦ ‖f x‖) s

Tactic:
fun x hx => (h x hx).norm'

Premises used: ContinuousOn, ContinuousWithinAt.norm'
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
inst_1 : TopologicalSpace α
f : α → E
s : Set α
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ≥0) (fun (x : α) ↦ ‖f x‖₊) s

Tactic:
fun x hx => (h x hx).nnnorm'

Premises used: ContinuousWithinAt.nnnorm', ContinuousOn
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedGroup E
l : Filter α
f : α → E
h : Tendsto (β := ℝ) (fun (y : α) ↦ ‖f y‖) l atTop
x : E
⊢ ∀ᶠ (y : α) in l, f y ≠ x

Tactic:
(h.eventually_ne_atTop _).mono fun _x => ne_of_apply_ne norm

Premises used: Norm.norm, Filter.Tendsto.eventually_ne_atTop, ne_of_apply_ne, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedGroup E
s : Set E
a : E
⊢ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a⁻¹ * b‖ < ε

Tactic:
simp [Metric.mem_closure_iff, dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul, Metric.mem_closure_iff
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε

Tactic:
simp only [tendstoUniformlyOn_iff, Pi.one_apply, dist_one_left]

Premises used: Pi.one_apply, Metric.tendstoUniformlyOn_iff, dist_one_left
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
⊢ UniformCauchySeqOnFilter f l l' ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'

Tactic:
⟨fun hf u hu => ?_, fun hf u hu => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
refine_1 :
  ∀ (hf : UniformCauchySeqOnFilter f l l') (u : Set (G × G)) (hu : u ∈ 𝓤 G),
    ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
      (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u
refine_2 :
  ∀
    (hf :
      TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l')
    (u : Set (G × G)) (hu : u ∈ 𝓤 G),
    ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u
⊢ UniformCauchySeqOnFilter f l l' ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'

Tactic:
refine ⟨fun hf u hu => ?_, fun hf u hu => ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
refine_1 :
  ∀ (ε : ℝ) (hε : 0 < ε)
    (H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u),
    ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
      (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u
⊢ ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
    (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u

Tactic:
obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu

Premises used: Filter.HasBasis.mem_uniformity_iff, Metric.uniformity_basis_dist, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u
⊢ ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
    (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u

Tactic:
(hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H 1 ((f x.fst.fst x.snd)⁻¹ * f x.fst.snd x.snd) ?_

Premises used: HMul.hMul, setOf, Prod.fst, Filter.Eventually.mono, Inv.inv, LT.lt, Dist.dist, OfNat.ofNat, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u
refine_1 :
  ∀ (x : Prod.{u_2, u_3} (ι × ι) κ)
    (hx : Membership.mem (γ := Set (G × G)) {p : G × G | dist p.1 p.2 < ε} (f x.1.1 x.2, f x.1.2 x.2)),
    Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (1, (f x.1.1 x.2)⁻¹ * f x.1.2 x.2)
⊢ ∀ᶠ (n : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l',
    (1 n.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) n.1 n.2) ∈ u

Tactic:
refine
      (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H 1 ((f x.fst.fst x.snd)⁻¹ * f x.fst.snd x.snd) ?_

Premises used: HMul.hMul, setOf, Prod.fst, Filter.Eventually.mono, Inv.inv, LT.lt, Dist.dist, OfNat.ofNat, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u
x : Prod.{u_2, u_3} (ι × ι) κ
hx : Membership.mem (γ := Set (G × G)) {p : G × G | dist p.1 p.2 < ε} (f x.1.1 x.2, f x.1.2 x.2)
⊢ Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (1, (f x.1.1 x.2)⁻¹ * f x.1.2 x.2)

Tactic:
simpa [dist_eq_norm_inv_mul, norm_div_rev] using hx

Premises used: dist_eq_norm_inv_mul, norm_div_rev
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
refine_2 :
  ∀ (ε : ℝ) (hε : 0 < ε)
    (H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u),
    ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u
⊢ ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u

Tactic:
obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu

Premises used: Filter.HasBasis.mem_uniformity_iff, Metric.uniformity_basis_dist, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u
⊢ ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u

Tactic:
(hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H (f x.fst.fst x.snd) (f x.fst.snd x.snd) ?_

Premises used: setOf, Prod.fst, Filter.Eventually.mono, LT.lt, Dist.dist, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u
refine_2 :
  ∀ (x : Prod.{u_2, u_3} (ι × ι) κ)
    (hx :
      Membership.mem.{u_6, u_6} (γ := Set (G × G)) {p : G × G | dist p.1 p.2 < ε}
        (1 x.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) x.1 x.2)),
    Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (f x.1.1 x.2, f x.1.2 x.2)
⊢ ∀ᶠ (m : Prod.{u_2, u_3} (ι × ι) κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u

Tactic:
refine
      (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
        H (f x.fst.fst x.snd) (f x.fst.snd x.snd) ?_

Premises used: setOf, Prod.fst, Filter.Eventually.mono, LT.lt, Dist.dist, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (a, b) → (a, b) ∈ u
x : Prod.{u_2, u_3} (ι × ι) κ
hx :
  Membership.mem.{u_6, u_6} (γ := Set (G × G)) {p : G × G | dist p.1 p.2 < ε}
    (1 x.2, (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) x.1 x.2)
⊢ Membership.mem (γ := SetRel G G) {p : G × G | dist p.1 p.2 < ε} (f x.1.1 x.2, f x.1.2 x.2)

Tactic:
simpa [dist_eq_norm_inv_mul, norm_div_rev] using hx

Premises used: dist_eq_norm_inv_mul, norm_div_rev
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
ι : Type u_2
κ : Type u_3
G : Type u_6
inst : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
rw :
  UniformCauchySeqOn f l s ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
rw₁ :
  UniformCauchySeqOnFilter f l (𝓟 s) ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
rw₂ rw₃ :
  TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s) ↔
    TendstoUniformlyOnFilter.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) (𝓟 s)
⊢ UniformCauchySeqOn f l s ↔
    TendstoUniformlyOn.{u_3, u_6, u_2} (β := G) (fun (n : ι × ι) (z : κ) ↦ (f n.1 z)⁻¹ * f n.2 z) 1 (l ×ˢ l) s

Tactic:
rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter,
    uniformCauchySeqOn_iff_uniformCauchySeqOnFilter,
    SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one]

Premises used: SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, uniformCauchySeqOn_iff_uniformCauchySeqOnFilter
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
α : Type u_1
E : Type u_4
inst : SeminormedCommGroup E
f : α → E
a : Filter α
b : E
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (β := ℝ) (fun (e : α) ↦ ‖f e / b‖) a (𝓝 0)

Tactic:
simp only [← dist_eq_norm_div, ← tendsto_iff_dist_tendsto_zero]

Premises used: dist_eq_norm_div, tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Set E
⊢ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε

Tactic:
simp [Metric.mem_closure_iff, dist_eq_norm_div]

Premises used: Metric.mem_closure_iff, dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
x : E
⊢ Tendsto (β := ℝ) (fun (a : E) ↦ ‖a / x‖) (𝓝 x) (𝓝 0)

Tactic:
simpa [dist_eq_norm_div] using
    tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (x : E)) (𝓝 x) _)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.dist, dist_eq_norm_div
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
x : E
⊢ ∀ᶠ (n : E) in 𝓝 x, Membership.mem (γ := Set ℝ) (Set.Ici 0) ‖n / x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
obtain :
  ∀ (u : ℕ → E) (u_in : ∀ (n : ℕ), u n ∈ s) (lim_u : Tendsto u atTop (𝓝 a)),
    ∃ (v : ℕ → E),
      Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
        (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
obtain ⟨u : ℕ → E, u_in : ∀ n, u n ∈ s, lim_u : Tendsto u atTop (𝓝 a)⟩ :=
    mem_closure_iff_seq_limit.mp hg

Premises used: mem_closure_iff_seq_limit, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
simp_rw : {x : E | dist x a < b 0} ∈ 𝓝 a
⊢ {x : E | ‖x⁻¹ * a‖ < b 0} ∈ 𝓝 a

Tactic:
simp_rw [← dist_eq_norm_inv_mul]

Premises used: dist_eq_norm_inv_mul
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
⊢ {x : E | dist x a < b 0} ∈ 𝓝 a

Tactic:
Metric.ball_mem_nhds _ (b_pos _)

Premises used: Set.Mem, setOf, Metric.ball, Metric.ball_mem_nhds
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
⊢ {x : E | dist x a < b 0} ∈ 𝓝 a

Tactic:
exact Metric.ball_mem_nhds _ (b_pos _)

Premises used: Metric.ball_mem_nhds
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
obtain :
  ∀ (n₀ : ℕ) (hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0),
    ∃ (v : ℕ → E),
      Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
        (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
obtain ⟨n₀, hn₀⟩ : ∃ n₀, ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0 :=
    haveI : { x | ‖x⁻¹ * a‖ < b 0 } ∈ 𝓝 a := by
      simp_rw [← dist_eq_norm_inv_mul]
      exact Metric.ball_mem_nhds _ (b_pos _)
    Filter.tendsto_atTop'.mp lim_u _ this

Premises used: Norm.norm, HMul.hMul, setOf, Inv.inv, LT.lt, Iff.mp, Filter.tendsto_atTop', OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
⊢ Tendsto z atTop (𝓝 a)

Tactic:
have lim_z : Tendsto z atTop (𝓝 a) := lim_u.comp (tendsto_add_atTop_nat n₀)
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
n : ℕ
⊢ {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E

Tactic:
simpa [← dist_eq_norm_inv_mul] using Metric.dist_mem_uniformity (b_pos <| n + 1)

Premises used: dist_eq_norm_inv_mul, HAdd.hAdd, OfNat.ofNat, Metric.dist_mem_uniformity
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
⊢ ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E

Tactic:
have mem_𝓤 : ∀ n, { p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1) } ∈ 𝓤 E := fun n => by
    simpa [← dist_eq_norm_inv_mul] using Metric.dist_mem_uniformity (b_pos <| n + 1)
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
obtain :
  ∀ (φ : ℕ → ℕ) (φ_extr : StrictMono φ) (hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)),
    ∃ (v : ℕ → E),
      Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
        (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
obtain ⟨φ : ℕ → ℕ, φ_extr : StrictMono φ, hφ : ∀ n, ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)⟩ :=
    lim_z.cauchySeq.subseq_mem mem_𝓤

Premises used: Filter.Tendsto.cauchySeq, CauchySeq.subseq_mem
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
⊢ Tendsto w atTop (𝓝 a)

Tactic:
have hw : Tendsto w atTop (𝓝 a) := lim_z.comp φ_extr.tendsto_atTop
-- Module: Mathlib.Analysis.Normed.Group.Continuity
Goal:
E : Type u_4
inst : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set E)
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun (n : ℕ) ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p : E × E | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun (i : ℕ) ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ ∃ (v : ℕ → E),
    Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
⟨v, ?_, ?_, hn₀ _ (n₀.le_add_left _), ?_⟩

Premises used: Nat.le_add_left, And.intro, Exists.intro