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 : α → 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 ∧
            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)

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 ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)) →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
refine_2 :
  ∀ (x : ιE),
    pE x →
      ∀ ⦃s t : Set F⦄,
        s ⊆ t →
          (l.EventuallyLE (β := ℝ≥0∞) (fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) fun (x : α) ↦ egauge 𝕜 t (g x)) →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) fun (x : α) ↦ egauge 𝕜 s (g x)
⊢ (∀ (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)

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 : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)

Tactic:
⟨V, hV₀, hV.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 : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)

Tactic:
exact ⟨V, hV₀, hV.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 →
      (l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦ egauge 𝕜 t (g x)) →
        l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦ egauge 𝕜 s (g x)

Tactic:
fun s t hsub h ↦ h.mono fun x hx ↦ hx.trans <| egauge_anti 𝕜 hsub (g x)

Premises used: Filter.Eventually.mono, LE.le.trans, egauge_anti, 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
⊢ ∀ ⦃s t : Set F⦄,
    s ⊆ t →
      (l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦ egauge 𝕜 t (g x)) →
        l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦ egauge 𝕜 s (g x)

Tactic:
exact fun s t hsub h ↦ h.mono fun x hx ↦ hx.trans <| egauge_anti 𝕜 hsub (g x)
-- 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 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
rw :
  ∀ (i : ι),
    p i →
      ∃ (j : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
⊢ f =O[𝕜; l] g

Tactic:
rw [hb.isBigOTVS_iff (basis_sets _)]

Premises used: Filter.basis_sets, Filter.HasBasis.isBigOTVS_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
inst_7 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
rcases :
  ∀ (C : ℝ≥0) (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
    (hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)),
    ∃ (j : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
⊢ ∃ (j : Set F), Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)

Tactic:
rcases h i hi with ⟨C, V, hV₀, 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
inst_7 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
rcases :
  ∀ (c : 𝕜) (hc : C < ‖c‖₊),
    ∃ (j : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
⊢ ∃ (j : Set F), Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)

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

Premises used: NormedField.exists_lt_nnnorm
-- 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 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
hc : C < nnnorm.{u_3} (E := 𝕜) 0
⊢ False

Tactic:
simp at 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 : α → F
inst_7 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
⊢ c ≠ 0

Tactic:
have hc₀ : c ≠ 0 := by rintro rfl; simp at 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 : α → F
inst_7 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
⊢ ∃ (j : Set F), Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)

Tactic:
⟨c⁻¹ • V, (set_smul_mem_nhds_zero_iff <| inv_ne_zero hc₀).mpr hV₀, ?_⟩

Premises used: Iff.mpr, set_smul_mem_nhds_zero_iff, Inv.inv, And.intro, Exists.intro, inv_ne_zero, HSMul.hSMul
-- 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 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
refine : ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)
⊢ ∃ (j : Set F), Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)

Tactic:
refine ⟨c⁻¹ • V, (set_smul_mem_nhds_zero_iff <| inv_ne_zero hc₀).mpr 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
inst_7 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)

Tactic:
hV.trans <| .of_forall fun x ↦ ?_

Premises used: Filter.Eventually.of_forall, Filter.EventuallyLE, Filter.EventuallyLE.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 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
refine :
  ∀ (x : α),
    LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)) x)
      ((fun (x : α) ↦ egauge 𝕜 (id (c⁻¹ • V)) (g x)) x)
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)

Tactic:
refine hV.trans <| .of_forall fun x ↦ ?_

Premises used: Filter.EventuallyLE.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 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
x : α
grw : (↑‖c‖₊ : ℝ≥0∞) * egauge 𝕜 V (g x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)
⊢ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)

Tactic:
grw [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 : α → F
inst_7 : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : HasBasis (𝓝 0) p U
h :
  ∀ (i : ι),
    p i →
      ∃ (C : ℝ≥0) (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 (U i) (f x)) fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)
c : 𝕜
hc : C < ‖c‖₊
hc₀ : c ≠ 0
x : α
⊢ (↑‖c‖₊ : ℝ≥0∞) * egauge 𝕜 V (g x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)

Tactic:
simp [egauge_smul_left, hc₀, enorm_eq_nnnorm, ENNReal.div_eq_inv_mul]

Premises used: enorm_eq_nnnorm, ENNReal.div_eq_inv_mul, egauge_smul_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
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V₁ V₂ : Set F
hV : V₁ ⊆ V₂
hV₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V₂ (g x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V₂ (g x)
⊢ (↑ε : ℝ≥0∞) * egauge 𝕜 V₂ (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V₁ (g x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V₁ V₂ : Set F
hV : V₁ ⊆ V₂
hV₂ : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 V₂ (g x)
x : α
hx : egauge 𝕜 U (f x) ≤ egauge 𝕜 V₂ (g x)
⊢ egauge 𝕜 V₂ (g x) ≤ egauge 𝕜 V₁ (g x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
β : Type u_2
𝕜 : 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
k : β → α
l : Filter β
⊢ f =o[𝕜; map k l] g ↔ (f ∘ k) =o[𝕜; l] (g ∘ k)

Tactic:
simp [isLittleOTVS_iff, EventuallyLE]

Premises used: Asymptotics.isLittleOTVS_iff, Filter.EventuallyLE
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
β : Type u_2
𝕜 : 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
k : β → α
l : Filter β
⊢ f =O[𝕜; map k l] g ↔ (f ∘ k) =O[𝕜; l] (g ∘ k)

Tactic:
simp [isBigOTVS_iff, EventuallyLE]

Premises used: Asymptotics.isBigOTVS_iff, 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₁ l₂ : Filter α
f : α → E
g : α → F
hf : f =o[𝕜; l₁] g
h : l₂ ≤ l₁
⊢ f =o[𝕜; l₂] g

Tactic:
⟨fun U hU ↦ let ⟨V, hV0, hV⟩ := hf.1 U hU; ⟨V, hV0, fun ε hε ↦ (hV ε hε).filter_mono h⟩⟩

Premises used: Filter.Eventually.filter_mono, Asymptotics.IsLittleOTVS.exists_eventuallyLE_mul, Membership.mem, Exists, nhds, And, Asymptotics.IsLittleOTVS.mk, And.intro, Exists.intro, _private.0.Asymptotics.IsLittleOTVS.mono.match_1, 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₁ l₂ : Filter α
f : α → E
g : α → F
hf : f =O[𝕜; l₁] g
h : l₂ ≤ l₁
⊢ f =O[𝕜; l₂] g

Tactic:
⟨fun U hU ↦ let ⟨V, hV0, hV⟩ := hf.1 U hU; ⟨V, hV0, hV.filter_mono h⟩⟩

Premises used: Filter.Eventually.filter_mono, Membership.mem, Exists, nhds, Asymptotics.IsBigOTVS.exists_eventuallyLE, And, And.intro, _private.0.Asymptotics.IsBigOTVS.mono.match_1, Exists.intro, Filter.EventuallyLE, OfNat.ofNat, Asymptotics.IsBigOTVS.mk, egauge
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
β : Type u_2
𝕜 : 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
k : β → α
lb : Filter β
h : f =o[𝕜; l] g
hk : Tendsto k lb l
⊢ (f ∘ k) =o[𝕜; lb] (g ∘ k)

Tactic:
isLittleOTVS_map.mp (h.mono hk)

Premises used: Asymptotics.isLittleOTVS_map, Iff.mp, Asymptotics.IsLittleOTVS.mono
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
β : Type u_2
𝕜 : 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
k : β → α
lb : Filter β
h : f =O[𝕜; l] g
hk : Tendsto k lb l
⊢ (f ∘ k) =O[𝕜; lb] (g ∘ k)

Tactic:
isBigOTVS_map.mp (h.mono hk)

Premises used: Iff.mp, Asymptotics.isBigOTVS_map, Asymptotics.IsBigOTVS.mono
-- 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₁ l₂ : Filter α
f : α → E
g : α → F
⊢ f =o[𝕜; l₁ ⊔ l₂] g ↔ f =o[𝕜; l₁] g ∧ f =o[𝕜; l₂] g

Tactic:
simp only [isLittleOTVS_iff_smallSets, ← forall_and, ← eventually_and, eventually_sup]

Premises used: Filter.eventually_and, Asymptotics.isLittleOTVS_iff_smallSets, Filter.eventually_sup, forall_and
-- 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₁ l₂ : Filter α
f : α → E
g : α → F
hf₁ : f =o[𝕜; l₁] g
hf₂ : f =o[𝕜; l₂] g
⊢ f =o[𝕜; l₁ ⊔ l₂] g

Tactic:
isLittleOTVS_sup.mpr ⟨hf₁, hf₂⟩

Premises used: Iff.mpr, And.intro, Asymptotics.isLittleOTVS_sup
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
𝕜 : 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 E
f : E →L[𝕜] F
⊢ IsBigOTVS.{u_3, u_4, u_5, u_4} 𝕜 (E := F) l (⇑f : (a : E) → F) id

Tactic:
⟨fun U hU ↦ ⟨f ⁻¹' U, (map_continuous f).tendsto' 0 0 (map_zero f) hU, .of_forall <|
    (mapsTo_preimage f U).egauge_le 𝕜 f⟩⟩

Premises used: map_zero, Filter.Eventually.of_forall, Set.mapsTo_preimage, Set.preimage, And.intro, Set.MapsTo.egauge_le, Exists.intro, ContinuousMapClass.map_continuous, Continuous.tendsto', OfNat.ofNat, Asymptotics.IsBigOTVS.mk, DFunLike.coe