awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ f =O[𝕜; l] f

Tactic:
.refl f l

Premises used: Asymptotics.IsBigOTVS.refl
-- 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
f : α → E
l : Filter α
⊢ f =Θ[𝕜; l] f

Tactic:
⟨.rfl, .rfl⟩

Premises used: Asymptotics.IsBigOTVS.rfl, And.intro, Asymptotics.IsThetaTVS
-- 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
⊢ f =Θ[𝕜; l] f

Tactic:
.refl f l

Premises used: Asymptotics.IsThetaTVS.refl
-- 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
⊢ f =O[𝕜; l] g

Tactic:
⟨fun U hU ↦ ?_⟩

Premises used: Asymptotics.IsBigOTVS.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
l : Filter α
f : α → E
g : α → F
h : f =o[𝕜; l] g
refine :
  ∀ (U : Set E) (hU : 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 x)
⊢ f =O[𝕜; l] 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
l : Filter α
f : α → E
g : α → F
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
rcases :
  ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
    (hV :
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)),
    ∃ (V : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) V ∧
        l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)

Tactic:
rcases h.1 U hU with ⟨V, hV₀, hV⟩

Premises used: Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul
-- 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
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
right : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g 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 : α → F
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)

Tactic:
simpa using hV 1 one_ne_zero

Premises used: one_ne_zero, OfNat.ofNat
-- 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 =Θ[𝕜; l] g
⊢ f =O[𝕜; l] g

Tactic:
h.left

Premises used: And.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
h : f =Θ[𝕜; l] g
⊢ g =Θ[𝕜; l] f

Tactic:
And.symm h

Premises used: And.symm, Asymptotics.IsThetaTVS
-- 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
⊢ f =Θ[𝕜; l] g ↔ g =Θ[𝕜; l] f

Tactic:
and_comm

Premises used: and_comm, Asymptotics.IsThetaTVS
-- 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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
⊢ f =O[𝕜; l] k

Tactic:
⟨fun U hU₀ ↦ ?_⟩

Premises used: Asymptotics.IsBigOTVS.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
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
refine :
  ∀ (U : Set E) (hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U),
    ∃ (V : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) V ∧
        l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)
⊢ f =O[𝕜; l] k

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
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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
obtain :
  ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
    (hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)),
    ∃ (V : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) V ∧
        l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)

Tactic:
obtain ⟨V, hV₀, hV⟩ := hfg.1 U hU₀

Premises used: Asymptotics.IsBigOTVS.exists_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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
obtain :
  ∀ (W : Set G) (hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W)
    (hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)),
    ∃ (V : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) V ∧
        l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)

Tactic:
obtain ⟨W, hW₀, hW⟩ := hgk.1 V hV₀

Premises used: Asymptotics.IsBigOTVS.exists_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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
refine : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 W (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
x : α
hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)

Tactic:
hx₁.trans hx₂

Premises used: LE.le.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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x) ((fun (x : α) ↦ egauge 𝕜 V (g x)) x))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 V (g x)) x) ((fun (x : α) ↦ egauge 𝕜 W (k x)) x))
                      x}
                  x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x) ((fun (x : α) ↦ egauge 𝕜 W (k x)) x))
                      x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (x : α) (hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)) (hx₂ : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)),
    egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 W (k x)

Tactic:
filter_upwards [hV, hW] with x hx₁ hx₂ using hx₁.trans hx₂
-- 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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =Θ[𝕜; l] k
⊢ f =O[𝕜; l] k

Tactic:
hfg.trans hgk.isBigOTVS

Premises used: Asymptotics.IsThetaTVS.isBigOTVS, 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
k : α → G
hfg : f =Θ[𝕜; l] g
hgk : g =O[𝕜; l] k
⊢ f =O[𝕜; l] k

Tactic:
hfg.isBigOTVS.trans hgk

Premises used: Asymptotics.IsThetaTVS.isBigOTVS, 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
k : α → G
hfg : f =Θ[𝕜; l] g
hgk : g =Θ[𝕜; l] k
⊢ f =Θ[𝕜; l] k

Tactic:
⟨hfg.1.trans hgk.1, hgk.2.trans hfg.2⟩

Premises used: And.right, And.left, And.intro, Asymptotics.IsBigOTVS.trans, Asymptotics.IsThetaTVS
-- 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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
⊢ f =o[𝕜; l] k

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
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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
refine :
  ∀ (U : Set E) (hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U),
    ∃ (V : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) V ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
⊢ f =o[𝕜; l] k

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
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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
obtain :
  ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
    (hV :
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)),
    ∃ (V : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) V ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)

Tactic:
obtain ⟨V, hV₀, hV⟩ := hfg.1 U hU₀

Premises used: Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul
-- 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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
obtain :
  ∀ (W : Set G) (hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W)
    (hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)),
    ∃ (V : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) V ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)

Tactic:
obtain ⟨W, hW₀, hW⟩ := hgk.1 V hV₀

Premises used: Asymptotics.IsBigOTVS.exists_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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
refine :
  ∀ (ε : ℝ≥0) (hε : ε ≠ 0),
    l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)

Tactic:
gcongr