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
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
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x)
                    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * 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 : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)) x))
                      x}
                  x}
            x}
      a
h₁ h₂ :
  ∀ (x : α) (hx₁ : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) (hx₂ : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)),
    egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)

Tactic:
filter_upwards [hV ε hε, hW] with x hx₁ hx₂ using hx₁.trans <| by gcongr
-- 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_isBigOTVS hgk.isBigOTVS

Premises used: Asymptotics.IsLittleOTVS.trans_isBigOTVS, Asymptotics.IsThetaTVS.isBigOTVS
-- 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 : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ 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.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 :
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g 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)
⊢ ∃ (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.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 : 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 :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g 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:
⟨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 : 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 :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * 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 : 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 :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx₁ : egauge 𝕜 U (f x) ≤ egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
⊢ egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * 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 :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
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 : α) ↦ (↑ε : ℝ≥0∞) * 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 : α) ↦ (↑ε : ℝ≥0∞) * 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) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)),
    egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)

Tactic:
filter_upwards [hV, hW ε hε] 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 =Θ[𝕜; l] g
hgk : g =o[𝕜; l] k
⊢ f =o[𝕜; l] k

Tactic:
hfg.isBigOTVS.trans_isLittleOTVS hgk

Premises used: Asymptotics.IsBigOTVS.trans_isLittleOTVS, Asymptotics.IsThetaTVS.isBigOTVS
-- 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:
hfg.trans_isBigOTVS hgk.isBigOTVS

Premises used: Asymptotics.IsLittleOTVS.trans_isBigOTVS, Asymptotics.IsLittleOTVS.isBigOTVS
-- 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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
rw :
  (∀ (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)) ↔
    ∀ (i : ιE),
      pE i →
        ∃ (j : ιF),
          pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (sF j) (g x)
⊢ f =o[𝕜; l] g ↔
    ∀ (i : ιE),
      pE i →
        ∃ (j : ιF),
          pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (sF j) (g x)

Tactic:
rw [isLittleOTVS_iff]

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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
⊢ (∀ (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)) ↔
    ∀ (i : ιE),
      pE i →
        ∃ (j : ιF),
          pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (sF j) (g x)

Tactic:
(hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_iff ?_

Premises used: Filter.HasBasis.exists_iff, forall₂_congr, Iff.trans, Filter.HasBasis.forall_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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
refine_1 :
  ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (ε : ℝ≥0),
              ε ≠ 0 →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (ε : ℝ≥0),
              ε ≠ 0 →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
refine_2 :
  ∀ (x : ιE),
    pE x →
      ∀ ⦃s t : Set F⦄,
        s ⊆ t →
          (∀ (ε : ℝ≥0),
              ε ≠ 0 →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) →
            ∀ (ε : ℝ≥0),
              ε ≠ 0 →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 s (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 (f x)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE),
      pE i →
        ∃ (j : ιF),
          pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (sF j) (g x)

Tactic:
refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_iff ?_

Premises used: Filter.HasBasis.exists_iff, forall₂_congr, Iff.trans, Filter.HasBasis.forall_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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
s t : Set E
hsub : s ⊆ t
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩

Premises used: Filter.Eventually.mono, And.intro, Exists.intro, egauge_anti, le_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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
s t : Set E
hsub : s ⊆ t
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
exact ⟨V, hV₀, fun ε hε ↦ (hV ε hε).mono fun x ↦ le_trans <| egauge_anti _ hsub _⟩
-- 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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
x : ιE
h : pE x
⊢ ∀ ⦃s t : Set F⦄,
    s ⊆ t →
      (∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦
              (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) →
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦
              (↑ε : ℝ≥0∞) * egauge 𝕜 s (g x)

Tactic:
fun s t hsub h ε hε ↦ (h ε hε).mono fun x hx ↦ hx.trans ?_

Premises used: Filter.Eventually.mono, LE.le.trans, Filter.EventuallyLE
-- 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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
x : ιE
h : pE x
refine_2 :
  ∀ (s t : Set F) (hsub : s ⊆ t)
    (h :
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦
            (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x))
    (ε : ℝ≥0) (hε : ε ≠ 0) (x_1 : α)
    (hx :
      LE.le (α := ℝ≥0∞) ((fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) x_1)
        ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) x_1)),
    LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) x_1)
      ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 s (g x)) x_1)
⊢ ∀ ⦃s t : Set F⦄,
    s ⊆ t →
      (∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦
              (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) →
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦
              (↑ε : ℝ≥0∞) * egauge 𝕜 s (g x)

Tactic:
refine fun s t hsub h ε hε ↦ (h ε hε).mono fun x hx ↦ hx.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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
x_1 : ιE
h_1 : pE x_1
s t : Set F
hsub : s ⊆ t
h :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 →
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (sE x_1) (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 (sE x_1) (f x)) x) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) x)
⊢ (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 s (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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
rw :
  (∀ (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 x)) ↔
    ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)
⊢ f =O[𝕜; l] g ↔ ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)

Tactic:
rw [isBigOTVS_iff]

Premises used: Asymptotics.isBigOTVS_iff