awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
⊢ IsLittleOTVS 𝕜 (E := E × F) l (fun (x : α) ↦ (f x, g x)) k ↔ f =o[𝕜; l] k ∧ g =o[𝕜; l] k

Tactic:
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.elim .prodMk⟩

Premises used: Asymptotics.IsLittleOTVS.prodMk, Asymptotics.IsLittleOTVS.fst, And.elim, Asymptotics.IsLittleOTVS.snd, And.intro, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
rw :
  ∀ (i : Prod.{u_4, u_5} (Set E) (Set F)),
    (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
        Membership.mem (γ := Filter F) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2 →
      ∃ (j : Set G),
        Membership.mem (γ := Filter G) (𝓝 0) j ∧
          ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
⊢ IsBigOTVS 𝕜 (E := E × F) l (fun (x : α) ↦ (f x, g x)) k

Tactic:
rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isBigOTVS_iff (basis_sets _)]

Premises used: nhds_basis_balanced, Filter.basis_sets, Filter.HasBasis.prod_nhds, Filter.HasBasis.isBigOTVS_iff
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : Membership.mem (γ := Filter E) (𝓝 0) (U, V).1
hUb : Balanced 𝕜 (U, V).1
hV : Membership.mem (γ := Filter F) (𝓝 0) (U, V).2
hVb : Balanced 𝕜 (U, V).2
rcases :
  ∀ (W : Set G) (hW : Membership.mem (γ := Filter G) (𝓝 0) W)
    (hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x))
    (hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)),
    ∃ (j : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) j ∧
        ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)

Tactic:
rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets
    with ⟨W, hW, hWf, hWg⟩

Premises used: Filter.Eventually.and, Asymptotics.IsBigOTVS.eventually_smallSets, Filter.Eventually.exists_mem_of_smallSets
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : Membership.mem (γ := Filter E) (𝓝 0) (U, V).1
hUb : Balanced 𝕜 (U, V).1
hV : Membership.mem (γ := Filter F) (𝓝 0) (U, V).2
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : Membership.mem (γ := Filter G) (𝓝 0) W
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)

Tactic:
⟨W, hW, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : Membership.mem (γ := Filter E) (𝓝 0) (U, V).1
hUb : Balanced 𝕜 (U, V).1
hV : Membership.mem (γ := Filter F) (𝓝 0) (U, V).2
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : Membership.mem (γ := Filter G) (𝓝 0) W
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
refine : ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id W) (k x)
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)

Tactic:
refine ⟨W, hW, ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : Membership.mem (γ := Filter E) (𝓝 0) (U, V).1
hUb : Balanced 𝕜 (U, V).1
hV : Membership.mem (γ := Filter F) (𝓝 0) (U, V).2
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : Membership.mem (γ := Filter G) (𝓝 0) W
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
h :
  ∀ (x : α) (hfx : egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)) (hgx : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)),
    egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ egauge 𝕜 (id W) (k x)
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id W) (k x)

Tactic:
filter_upwards [hWf, hWg] with x hfx hgx
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : Membership.mem (γ := Filter E) (𝓝 0) (U, V).1
hUb : Balanced 𝕜 (U, V).1
hV : Membership.mem (γ := Filter F) (𝓝 0) (U, V).2
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : Membership.mem (γ := Filter G) (𝓝 0) W
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
x : α
hfx : egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hgx : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ egauge 𝕜 (id W) (k x)

Tactic:
simp [egauge_prod_mk, *]

Premises used: egauge_prod_mk
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E × F
g : α → G
h : f =O[𝕜; l] g
⊢ IsBigOTVS.{u_3, u_1, u_4, u_6} 𝕜 (E := E) l (fun (x : α) ↦ (f x).1) g

Tactic:
ContinuousLinearMap.fst 𝕜 E F |>.isBigOTVS_comp |>.trans h

Premises used: ContinuousLinearMap.isBigOTVS_comp, ContinuousLinearMap.fst, Asymptotics.IsBigOTVS.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E × F
g : α → G
h : f =O[𝕜; l] g
⊢ IsBigOTVS.{u_3, u_1, u_5, u_6} 𝕜 (E := F) l (fun (x : α) ↦ (f x).2) g

Tactic:
ContinuousLinearMap.snd 𝕜 E F |>.isBigOTVS_comp |>.trans h

Premises used: ContinuousLinearMap.snd, ContinuousLinearMap.isBigOTVS_comp, Asymptotics.IsBigOTVS.trans
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
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
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
⊢ IsBigOTVS 𝕜 (E := E × F) l (fun (x : α) ↦ (f x, g x)) k ↔ f =O[𝕜; l] k ∧ g =O[𝕜; l] k

Tactic:
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.elim .prodMk⟩

Premises used: Asymptotics.IsBigOTVS.snd, And.elim, Asymptotics.IsBigOTVS.prodMk, And.intro, Iff.intro, Asymptotics.IsBigOTVS.fst
-- 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
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =o[𝕜; l] g
h₂ : f₂ =o[𝕜; l] g
⊢ (f₁ + f₂) =o[𝕜; l] g

Tactic:
ContinuousLinearMap.fst 𝕜 E E + ContinuousLinearMap.snd 𝕜 E E |>.isBigOTVS_comp
    |>.trans_isLittleOTVS <| h₁.prodMk h₂

Premises used: Asymptotics.IsLittleOTVS.prodMk, ContinuousLinearMap.snd, Asymptotics.IsBigOTVS.trans_isLittleOTVS, ContinuousLinearMap.isBigOTVS_comp, HAdd.hAdd, ContinuousLinearMap.fst
-- 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
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
f₁ f₂ : α → E
g : α → F
l : Filter α
h₁ : f₁ =O[𝕜; l] g
h₂ : f₂ =O[𝕜; l] g
⊢ (f₁ + f₂) =O[𝕜; l] g

Tactic:
ContinuousLinearMap.fst 𝕜 E E + ContinuousLinearMap.snd 𝕜 E E |>.isBigOTVS_comp
    |>.trans <| h₁.prodMk h₂

Premises used: ContinuousLinearMap.snd, Asymptotics.IsBigOTVS.prodMk, ContinuousLinearMap.isBigOTVS_comp, HAdd.hAdd, ContinuousLinearMap.fst, Asymptotics.IsBigOTVS.trans
-- 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
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
f₁ f₂ f₃ : α → E
g : α → F
l : Filter α
h₁ : (f₁ - f₂) =o[𝕜; l] g
h₂ : (f₂ - f₃) =o[𝕜; l] g
⊢ (f₁ - f₃) =o[𝕜; l] g

Tactic:
simpa using h₁.add h₂

Premises used: Asymptotics.IsLittleOTVS.add
-- 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
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
f₁ f₂ f₃ : α → E
g : α → F
l : Filter α
h₁ : (f₁ - f₂) =O[𝕜; l] g
h₂ : (f₂ - f₃) =O[𝕜; l] g
⊢ (f₁ - f₃) =O[𝕜; l] g

Tactic:
simpa using h₁.add h₂

Premises used: Asymptotics.IsBigOTVS.add
-- 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
inst_7 : ContinuousNeg E
h : f =O[𝕜; l] g
⊢ (-f) =O[𝕜; l] g

Tactic:
.trans ((ContinuousLinearMap.mk (-.id (R := 𝕜)) continuous_neg).isBigOTVS_comp) h

Premises used: Asymptotics.IsBigOTVS.trans
-- 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
inst_7 : ContinuousNeg E
h : (-f) =O[𝕜; l] g
⊢ f =O[𝕜; l] g

Tactic:
simpa using h.neg_left

Premises used: Asymptotics.IsBigOTVS.neg_left
-- 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
inst_7 : ContinuousNeg E
⊢ IsBigOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l (fun (x : α) ↦ -f x) g ↔ f =O[𝕜; l] g

Tactic:
isBigOTVS_neg_left

Premises used: Asymptotics.isBigOTVS_neg_left
-- 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
inst_7 : ContinuousNeg E
h : f =o[𝕜; l] g
⊢ (-f) =o[𝕜; l] g

Tactic:
IsBigOTVS.rfl.neg_left.trans_isLittleOTVS h

Premises used: Asymptotics.IsBigOTVS.trans_isLittleOTVS, Asymptotics.IsBigOTVS.rfl, Asymptotics.IsBigOTVS.neg_left
-- 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
inst_7 : ContinuousNeg E
h : (-f) =o[𝕜; l] g
⊢ f =o[𝕜; l] g

Tactic:
simpa using h.neg_left

Premises used: Asymptotics.IsLittleOTVS.neg_left
-- 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
inst_7 : ContinuousNeg E
⊢ IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l (fun (x : α) ↦ -f x) g ↔ f =o[𝕜; l] g

Tactic:
isLittleOTVS_neg_left

Premises used: Asymptotics.isLittleOTVS_neg_left
-- 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 α
g : α → F
inst_7 : ContinuousNeg E
f₁ f₂ : α → E
h : (f₁ - f₂) =o[𝕜; l] g
⊢ (f₂ - f₁) =o[𝕜; l] g

Tactic:
simpa using h.neg_left

Premises used: Asymptotics.IsLittleOTVS.neg_left
-- 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 α
g : α → F
inst_7 : ContinuousNeg E
f₁ f₂ : α → E
⊢ (f₁ - f₂) =o[𝕜; l] g ↔ (f₂ - f₁) =o[𝕜; l] g

Tactic:
⟨.symm, .symm⟩

Premises used: Iff.intro, Asymptotics.IsLittleOTVS.symm
-- 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 α
g : α → F
inst_7 : ContinuousNeg E
f₁ f₂ : α → E
⊢ IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l (fun (a : α) ↦ f₁ a - f₂ a) g ↔
    IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l (fun (a : α) ↦ f₂ a - f₁ a) g

Tactic:
isLittleOTVS_comm

Premises used: Asymptotics.isLittleOTVS_comm
-- 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 α
g : α → F
inst_7 : ContinuousNeg E
f₁ f₂ : α → E
h : (f₁ - f₂) =O[𝕜; l] g
⊢ (f₂ - f₁) =O[𝕜; l] g

Tactic:
simpa using h.neg_left

Premises used: Asymptotics.IsBigOTVS.neg_left
-- 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 α
g : α → F
inst_7 : ContinuousNeg E
f₁ f₂ : α → E
⊢ (f₁ - f₂) =O[𝕜; l] g ↔ (f₂ - f₁) =O[𝕜; l] g

Tactic:
⟨.symm, .symm⟩

Premises used: Asymptotics.IsBigOTVS.symm, Iff.intro
-- 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 α
g : α → F
inst_7 : ContinuousNeg E
f₁ f₂ : α → E
⊢ IsBigOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l (fun (a : α) ↦ f₁ a - f₂ a) g ↔
    IsBigOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l (fun (a : α) ↦ f₂ a - f₁ a) g

Tactic:
isBigOTVS_comm

Premises used: Asymptotics.isBigOTVS_comm
-- 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
inst_7 : ContinuousNeg F
h : f =O[𝕜; l] g
⊢ g =O[𝕜; l] (-g)

Tactic:
simpa using (IsBigOTVS.refl (-g) l).neg_left

Premises used: Asymptotics.IsBigOTVS.neg_left, Asymptotics.IsBigOTVS.refl, Neg.neg
-- 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
inst_7 : ContinuousNeg F
h : f =O[𝕜; l] (-g)
⊢ f =O[𝕜; l] g

Tactic:
simpa using h.neg_right

Premises used: Asymptotics.IsBigOTVS.neg_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
inst_7 : ContinuousNeg F
⊢ (IsBigOTVS.{u_3, u_1, u_4, u_5} 𝕜 (F := F) l f fun (x : α) ↦ -g x) ↔ f =O[𝕜; l] g

Tactic:
isBigOTVS_neg_right

Premises used: Asymptotics.isBigOTVS_neg_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
inst_7 : ContinuousNeg F
h : f =o[𝕜; l] g
⊢ f =o[𝕜; l] (-g)

Tactic:
h.trans_isBigOTVS (.neg_right .rfl)

Premises used: Asymptotics.IsBigOTVS.neg_right, Asymptotics.IsLittleOTVS.trans_isBigOTVS, Asymptotics.IsBigOTVS.rfl
-- 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
inst_7 : ContinuousNeg F
h : f =o[𝕜; l] (-g)
⊢ f =o[𝕜; l] g

Tactic:
simpa using h.neg_right

Premises used: Asymptotics.IsLittleOTVS.neg_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
inst_7 : ContinuousNeg F
⊢ (IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (F := F) l f fun (x : α) ↦ -g x) ↔ f =o[𝕜; l] g

Tactic:
isLittleOTVS_neg_right

Premises used: Asymptotics.isLittleOTVS_neg_right
-- 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
⊢ HasBasis (α := (i : ι) → E i) (Filter.pi (α := E) fun (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)

Tactic:
have := hasBasis_pi fun i ↦ nhds_basis_balanced 𝕜 (E i)
-- 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 :
  HasBasis (α := (i : ι) → E i) (Filter.pi (α := E) fun (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)
⊢ 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)

Tactic:
rw [← nhds_pi, ← Pi.zero_def] at this

Premises used: nhds_pi, Pi.zero_def