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
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 : E →L[𝕜] F
⊢ IsBigOTVS.{u_3, u_1, u_5, u_4} 𝕜 (E := F) l ((⇑g : (a : E) → F) ∘ f) f

Tactic:
g.isBigOTVS_id.comp_tendsto tendsto_top

Premises used: Asymptotics.IsBigOTVS.comp_tendsto, Filter.tendsto_top, ContinuousLinearMap.isBigOTVS_id
-- 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 : E →L[𝕜] F
⊢ IsBigOTVS.{u_3, u_1, u_5, u_4} 𝕜 (E := F) l (fun (x : α) ↦ (g : (a : E) → F) (f x)) f

Tactic:
g.isBigOTVS_comp

Premises used: ContinuousLinearMap.isBigOTVS_comp
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
exists_eventuallyLE :
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
            egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)
⊢ IsBigOTVS.{u_3, u_1, u_4, u_5} 𝕜 (F := F) l f ((⇑g : (a : E) → F) ∘ f)

Tactic:
constructor
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
exists_eventuallyLE :
  ∀ (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V) (hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U),
    ∃ (V : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) V ∧
        l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
          egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)

Tactic:
rcases mem_comap.1 (hg hU) with ⟨V, hV, hgV⟩

Premises used: Filter.mem_comap, Iff.mp
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
right :
  l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)

Tactic:
use V, hV
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
right : ∀ (a : α), egauge 𝕜 U (f a) ≤ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) a)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)

Tactic:
filter_upwards with a
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
⊢ egauge 𝕜 U (f a) ≤ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) a)

Tactic:
le_egauge_of_forall_ne_zero (mem_of_mem_nhds hV) fun c hc₀ hc ↦ ?_

Premises used: mem_of_mem_nhds, le_egauge_of_forall_ne_zero
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
right : ∀ (c : 𝕜) (hc₀ : c ≠ 0) (hc : ((⇑g : (a : E) → F) ∘ f) a ∈ c • V), egauge 𝕜 U (f a) ≤ ‖c‖ₑ
⊢ egauge 𝕜 U (f a) ≤ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) a)

Tactic:
refine le_egauge_of_forall_ne_zero (mem_of_mem_nhds hV) fun c hc₀ hc ↦ ?_

Premises used: mem_of_mem_nhds, le_egauge_of_forall_ne_zero
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : ((⇑g : (a : E) → F) ∘ f) a ∈ c • V
right : f a ∈ c • U
⊢ egauge 𝕜 U (f a) ≤ ‖c‖ₑ

Tactic:
apply egauge_le_of_mem_smul

Premises used: egauge_le_of_mem_smul
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : ((⇑g : (a : E) → F) ∘ f) a ∈ c • V
right : Membership.mem (γ := Set E) ((⇑g : (a : E) → F) ⁻¹' (c • V)) (f a)
⊢ f a ∈ c • U

Tactic:
grw [← hgV, ← (IsUnit.mk0 _ hc₀).preimage_smul_set]

Premises used: IsUnit.preimage_smul_set, IsUnit.mk0
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : ((⇑g : (a : E) → F) ∘ f) a ∈ c • V
⊢ Membership.mem (γ := Set E) ((⇑g : (a : E) → F) ⁻¹' (c • V)) (f a)

Tactic:
hc

Premises used: Set.Mem, setOf, Set.preimage
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : ((⇑g : (a : E) → F) ∘ f) a ∈ c • V
⊢ Membership.mem (γ := Set E) ((⇑g : (a : E) → F) ⁻¹' (c • V)) (f a)

Tactic:
exact hc
-- 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 : E →L[𝕜] F
hg : Topology.IsInducing.{u_4, u_5} (X := E) (Y := F) (⇑g : (a : E) → F)
⊢ LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑(↑g : E →ₗ[𝕜] F) : (a : E) → F) (𝓝 0)) (𝓝 0)

Tactic:
simp [hg.nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap
-- 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
g : α → F
l : Filter α
⊢ IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l 0 g

Tactic:
⟨fun U hU ↦ ?_⟩

Premises used: Asymptotics.IsLittleOTVS.mk
-- 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
g : α → F
l : Filter α
refine :
  ∀ (U : Set E) (hU : Membership.mem (γ := Filter E) (𝓝 0) U),
    ∃ (V : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) V ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (0 x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l 0 g

Tactic:
refine ⟨fun U hU ↦ ?_⟩
-- 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
g : α → F
l : Filter α
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
h :
  Membership.mem (γ := Filter F) (𝓝 0) univ ∧
    ∀ (ε : ℝ≥0),
      ε ≠ 0 →
        l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (0 x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 univ (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (0 x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
use univ

Premises used: Set.univ
-- 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
g : α → F
l : Filter α
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ Membership.mem (γ := Filter F) (𝓝 0) univ ∧
    ∀ (ε : ℝ≥0),
      ε ≠ 0 →
        l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (0 x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 univ (g x)

Tactic:
simp [egauge_zero_right _ (Filter.nonempty_of_mem hU), EventuallyLE]

Premises used: Filter.nonempty_of_mem, Filter.EventuallyLE, egauge_zero_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
f : α → E
g : α → F
inst_7 : TopologicalSpace α
x : α
s : Set α
h : f x = 0
rw : f =o[𝕜; pure x] g
⊢ f =o[𝕜; 𝓝[insert x s] x] g ↔ f =o[𝕜; 𝓝[s] x] g

Tactic:
rw [nhdsWithin_insert, isLittleOTVS_sup, and_iff_right]

Premises used: nhdsWithin_insert, and_iff_right, Asymptotics.isLittleOTVS_sup
-- 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
f : α → E
g : α → F
inst_7 : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜; pure x] g

Tactic:
.congr' (.zero g _) h.symm .rfl

Premises used: Asymptotics.IsLittleOTVS.zero, Asymptotics.IsLittleOTVS.congr', Filter.EventuallyEq.rfl, Eq.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
f : α → E
g : α → F
inst_7 : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜; pure x] g

Tactic:
exact .congr' (.zero g _) h.symm .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
f : α → E
g : α → F
inst_7 : TopologicalSpace α
x : α
s : Set α
h : f =o[𝕜; 𝓝[s] x] g
hf : f x = 0
⊢ f =o[𝕜; 𝓝[Insert.insert x s] x] g

Tactic:
(isLittleOTVS_insert hf).2 h

Premises used: Iff.mpr, Asymptotics.isLittleOTVS_insert
-- 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
f : α → E
g : α → F
u : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) u
⊢ Membership.mem (γ := Filter F) (𝓝 0) univ ∧
    ∀ (ε : ℝ≥0),
      ε ≠ 0 →
        EventuallyLE (β := ℝ≥0∞) ⊥ (fun (x : α) ↦ egauge 𝕜 u (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 univ (g x)

Tactic:
simp [EventuallyLE]

Premises used: Filter.EventuallyLE
-- 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 ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id j) (k x)
⊢ IsLittleOTVS 𝕜 (E := E × F) l (fun (x : α) ↦ (f x, g x)) k

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

Premises used: Filter.HasBasis.isLittleOTVS_iff, nhds_basis_balanced, Filter.basis_sets, Filter.HasBasis.prod_nhds
-- 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 : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x))
    (hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)),
    ∃ (j : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) j ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id j) (k x)
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * 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: Asymptotics.IsLittleOTVS.eventually_smallSets, Filter.Eventually.and, 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 : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id j) (k x)

Tactic:
⟨W, hW, fun ε hε ↦ ?_⟩

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 : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
refine :
  ∀ (ε : ℝ≥0) (hε : ε ≠ 0),
    ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id W) (k x)
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id j) (k x)

Tactic:
refine ⟨W, hW, fun ε hε ↦ ?_⟩
-- 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 : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
h :
  ∀ (x : α) (hfx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x))
    (hgx : egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)),
    egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id W) (k x)
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id W) (k x)

Tactic:
filter_upwards [hWf ε hε, hWg ε hε] 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 : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hfx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
hgx : egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
⊢ egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ (↑ε : ℝ≥0∞) * 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
⊢ IsLittleOTVS.{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_isLittleOTVS h

Premises used: Asymptotics.IsBigOTVS.trans_isLittleOTVS, ContinuousLinearMap.isBigOTVS_comp, ContinuousLinearMap.fst
-- 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
⊢ IsLittleOTVS.{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_isLittleOTVS h

Premises used: ContinuousLinearMap.snd, Asymptotics.IsBigOTVS.trans_isLittleOTVS, ContinuousLinearMap.isBigOTVS_comp