awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I), ∀ᶠ (V : Set F) in smallSets (𝓝 0), ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
right :
  ∀ (x : α) (hx : ∀ i ∈ I, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)),
    (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 V (g x)
⊢ ∀ᶠ (x : α) in l,
    (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 V (g x)

Tactic:
refine (hIf.eventually_all.mpr hV).mono fun x hx ↦ ?_

Premises used: Iff.mpr, Set.Finite.eventually_all, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I), ∀ᶠ (V : Set F) in smallSets (𝓝 0), ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
x : α
hx : ∀ i ∈ I, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
⊢ (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 V (g x)

Tactic:
simpa only [id, egauge_pi hIf Ub, iSup₂_le_iff]

Premises used: egauge_pi, id, iSup₂_le_iff
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
f : α → (i : ι) → E i
h : f =O[𝕜; l] g
i : ι
⊢ IsBigOTVS.{u_3, u_1, u_8, u_5} 𝕜 (E := E i) l (fun (x : α) ↦ f x i) g

Tactic:
ContinuousLinearMap.proj i |>.isBigOTVS_fun_comp |>.trans h

Premises used: ContinuousLinearMap.isBigOTVS_fun_comp, Asymptotics.IsBigOTVS.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : α → (i : ι) → E i
⊢ f =O[𝕜; l] g ↔ ∀ (i : ι), IsBigOTVS.{u_3, u_1, u_8, u_5} 𝕜 (E := E i) l (fun (x : α) ↦ f x i) g

Tactic:
⟨.proj, .pi⟩

Premises used: Asymptotics.IsBigOTVS.proj, Iff.intro, Asymptotics.IsBigOTVS.pi
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
h : f =o[𝕜; l] g
c : α → 𝕜
simp :
  ∀
    (h :
      ∀ (U : Set E),
        Membership.mem (γ := Filter E) (𝓝 0) U →
          ∃ (V : Set F),
            Membership.mem (γ := Filter F) (𝓝 0) V ∧
              ∀ (ε : ℝ≥0),
                ε ≠ 0 →
                  l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
                    (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x))
    (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (c x • f x)) fun (x : α) ↦
                (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)
⊢ IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) (F := F) l (fun (x : α) ↦ c x • f x) fun (x : α) ↦ c x • g x

Tactic:
simp only [isLittleOTVS_iff] at *

Premises used: Asymptotics.isLittleOTVS_iff
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
h₁ :
  ∀ (U : Set E) (hU : Membership.mem (γ := Filter E) (𝓝 0) U) (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V)
    (ε : ℝ≥0) (hε : ε ≠ 0) (x : α)
    (hx : LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) x)),
    LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (c x • f x)) x)
      ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)) x)
⊢ ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (c x • f x)) fun (x : α) ↦
                (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)

Tactic:
peel h with U hU V hV ε hε x hx
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
h₁ : ‖c x‖ₑ * egauge 𝕜 U (f x) ≤ ‖c x‖ₑ * ((↑ε : ℝ≥0∞) * egauge 𝕜 V (g x))
h₂ : c x = 0 → V.Nonempty
h₃ : c x = 0 → U.Nonempty
⊢ egauge 𝕜 U (c x • f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)

Tactic:
rw [egauge_smul_right, egauge_smul_right, mul_left_comm]

Premises used: mul_left_comm, egauge_smul_right
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ‖c x‖ₑ * egauge 𝕜 U (f x) ≤ ‖c x‖ₑ * ((↑ε : ℝ≥0∞) * egauge 𝕜 V (g x))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ c x = 0 → V.Nonempty

Tactic:
fun _ ↦ Filter.nonempty_of_mem ‹_›

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ c x = 0 → V.Nonempty

Tactic:
exact fun _ ↦ Filter.nonempty_of_mem ‹_›

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ c x = 0 → U.Nonempty

Tactic:
fun _ ↦ Filter.nonempty_of_mem ‹_›

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
c : α → 𝕜
h :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ c x = 0 → U.Nonempty

Tactic:
exact fun _ ↦ Filter.nonempty_of_mem ‹_›

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
mp : IsLittleOTVS 𝕜 (F := 𝕜) l f 1 → Tendsto f l (𝓝 0)
mpr : Tendsto f l (𝓝 0) → IsLittleOTVS 𝕜 (F := 𝕜) l f 1
⊢ IsLittleOTVS 𝕜 (F := 𝕜) l f 1 ↔ Tendsto f l (𝓝 0)

Tactic:
constructor
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf : IsLittleOTVS 𝕜 (F := 𝕜) l f 1
⊢ ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)

Tactic:
rw [(basis_sets _).isLittleOTVS_iff nhds_basis_ball] at hf

Premises used: Filter.HasBasis.isLittleOTVS_iff, Filter.basis_sets, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
mp : ∀ (i : Set E), Membership.mem (γ := Filter E) (𝓝 0) i ∧ Balanced 𝕜 i → ∀ᶠ (x : α) in l, f x ∈ id i
⊢ Tendsto f l (𝓝 0)

Tactic:
rw [(nhds_basis_balanced 𝕜 E).tendsto_right_iff]

Premises used: nhds_basis_balanced, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
mp :
  ∀ (r : ℝ) (hr₀ : 0 < r)
    (hr :
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 r) (1 x)),
    ∀ᶠ (x : α) in l, f x ∈ id U
⊢ ∀ᶠ (x : α) in l, f x ∈ id U

Tactic:
rcases hf U hU with ⟨r, hr₀, hr⟩
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ
hr₀ : 0 < r
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 r) (1 x)
⊢ 0 ≤ r

Tactic:
hr₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ
hr₀ : 0 < r
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 r) (1 x)
mp :
  ∀ (r : ℝ≥0) (hr₀ : 0 < (↑r : ℝ))
    (hr :
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)),
    ∀ᶠ (x : α) in l, f x ∈ id U
⊢ ∀ᶠ (x : α) in l, f x ∈ id U

Tactic:
lift r to ℝ≥0 using hr₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr₀ : 0 < (↑r : ℝ)
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
⊢ 0 < r

Tactic:
norm_cast at hr₀
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
mp : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ∀ᶠ (x : α) in l, f x ∈ id U
⊢ ∀ᶠ (x : α) in l, f x ∈ id U

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Premises used: NormedField.exists_one_lt_norm
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
h : ∀ᶠ (x : ℝ≥0) in 𝓝 0, (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1
⊢ ∃ (ε : ℝ≥0), 0 < ε ∧ (↑ε : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1

Tactic:
apply Eventually.exists_gt

Premises used: Filter.Eventually.exists_gt
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ (↑0 : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
h : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞)
⊢ ∀ᶠ (x : ℝ≥0) in 𝓝 0, (↑x : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) / (↑r : ℝ≥0∞) < 1

Tactic:
refine Continuous.tendsto' ?_ _ _ (by simp) |>.eventually_lt_const zero_lt_one

Premises used: zero_lt_one, Filter.Tendsto.eventually_lt_const, Continuous.tendsto'
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ (↑r : ℝ≥0∞) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ (↑r : ℝ≥0∞) ≠ 0

Tactic:
first | apply ENNReal.coe_ne_top | positivity

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
l : Filter α
f : α → E
inst_4 : ContinuousSMul 𝕜 E
hf :
  ∀ (i : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 j) (1 x)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
hUb : Balanced 𝕜 U
r : ℝ≥0
hr :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ (↑ε : ℝ≥0∞) * egauge.{u_3, u_3} 𝕜 (E := 𝕜) (ball 0 (↑r : ℝ)) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ (↑‖c‖₊ : ℝ≥0∞) ≠ ∞

Tactic:
apply ENNReal.coe_ne_top

Premises used: ENNReal.coe_ne_top