awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
simp :
  ∀ (a : Set ι) (b : (i : ι) → Set (E i)),
    (a.Finite ∧
        (∀ (x : ι) (x_1 : x ∈ a), Membership.mem (γ := Filter (E x)) (𝓝 0) (b x)) ∧
          ∀ (x : ι) (x_1 : x ∈ a), Balanced 𝕜 (b x)) →
      ∃ (j : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) j ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              ∀ᶠ (x : α) in l,
                (egauge 𝕜 (E := (i : ι) → E i) (a.pi (α := E) fun (i : ι) ↦ b i) fun (i : ι) ↦ f i x) ≤
                  (↑ε : ℝ≥0∞) * egauge 𝕜 j (g x)
⊢ IsLittleOTVS 𝕜 (E := (i : ι) → E i) l (fun (x : α) (i : ι) ↦ f i x) g

Tactic:
simp only [this.isLittleOTVS_iff (basis_sets _), forall_and, Prod.forall, id]

Premises used: Filter.HasBasis.isLittleOTVS_iff, id, Filter.basis_sets, Prod.forall, forall_and
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
⊢ ∀ (i : ι) (hi : i ∈ I),
    ∀ᶠ (V : Set F) in smallSets (𝓝 0),
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
have := fun i hi ↦ (h i).eventually_smallSets (U i) (hU i hi)
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I),
    ∀ᶠ (V : Set F) in smallSets (𝓝 0),
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
rcases :
  ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
    (hV : ∀ i ∈ I, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)),
    ∃ (j : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) j ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            ∀ᶠ (x : α) in l,
              (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤
                (↑ε : ℝ≥0∞) * egauge 𝕜 j (g x)
⊢ ∃ (j : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          ∀ᶠ (x : α) in l,
            (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤
              (↑ε : ℝ≥0∞) * egauge 𝕜 j (g x)

Tactic:
rcases (hIf.eventually_all.mpr this).exists_mem_of_smallSets with ⟨V, hV₀, hV⟩

Premises used: Iff.mpr, Set.Finite.eventually_all, Filter.Eventually.exists_mem_of_smallSets
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I),
    ∀ᶠ (V : Set F) in smallSets (𝓝 0),
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∃ (j : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          ∀ᶠ (x : α) in l,
            (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤
              (↑ε : ℝ≥0∞) * egauge 𝕜 j (g x)

Tactic:
⟨V, hV₀, fun ε hε ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I),
    ∀ᶠ (V : Set F) in smallSets (𝓝 0),
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
refine :
  ∀ (ε : ℝ≥0) (hε : ε ≠ 0),
    ∀ᶠ (x : α) in l,
      (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤
        (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∃ (j : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 →
          ∀ᶠ (x : α) in l,
            (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤
              (↑ε : ℝ≥0∞) * egauge 𝕜 j (g x)

Tactic:
refine ⟨V, hV₀, fun ε hε ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I),
    ∀ᶠ (V : Set F) in smallSets (𝓝 0),
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∀ᶠ (x : α) in l,
    (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤
      (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
(hIf.eventually_all.mpr (hV · · ε hε)).mono fun x hx ↦ ?_

Premises used: Iff.mpr, Set.Finite.eventually_all, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I),
    ∀ᶠ (V : Set F) in smallSets (𝓝 0),
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : ε ≠ 0
refine :
  ∀ (x : α) (hx : ∀ i ∈ I, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)),
    (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤
      (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∀ᶠ (x : α) in l,
    (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤
      (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
refine (hIf.eventually_all.mpr (hV · · ε hε)).mono fun x hx ↦ ?_

Premises used: Iff.mpr, Set.Finite.eventually_all, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I),
    ∀ᶠ (V : Set F) in smallSets (𝓝 0),
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : ∀ i ∈ I, egauge 𝕜 (U i) (f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)

Tactic:
simpa only [id, egauge_pi hIf Ub, iSup₂_le_iff]

Premises used: egauge_pi, id, iSup₂_le_iff
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
f : α → (i : ι) → E i
h : f =o[𝕜; l] g
i : ι
⊢ IsLittleOTVS.{u_3, u_1, u_8, u_5} 𝕜 (E := E i) l (fun (x : α) ↦ f x i) g

Tactic:
ContinuousLinearMap.proj i |>.isBigOTVS_fun_comp |>.trans_isLittleOTVS h

Premises used: Asymptotics.IsBigOTVS.trans_isLittleOTVS, ContinuousLinearMap.isBigOTVS_fun_comp
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : α → (i : ι) → E i
⊢ f =o[𝕜; l] g ↔ ∀ (i : ι), IsLittleOTVS.{u_3, u_1, u_8, u_5} 𝕜 (E := E i) l (fun (x : α) ↦ f x i) g

Tactic:
⟨.proj, .pi⟩

Premises used: Asymptotics.IsLittleOTVS.pi, Iff.intro, Asymptotics.IsLittleOTVS.proj
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
⊢ HasBasis (α := (i : ι) → E i) (Filter.pi (α := E) fun (i : ι) ↦ 𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)

Tactic:
have := hasBasis_pi fun i ↦ nhds_basis_balanced 𝕜 (E i)
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this :
  HasBasis (α := (i : ι) → E i) (Filter.pi (α := E) fun (i : ι) ↦ 𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
⊢ HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)

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

Premises used: nhds_pi, Pi.zero_def
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
simp :
  ∀ (a : Set ι) (b : (i : ι) → Set (E i)),
    (a.Finite ∧
        (∀ (x : ι) (x_1 : x ∈ a), Membership.mem (γ := Filter (E x)) (𝓝 0) (b x)) ∧
          ∀ (x : ι) (x_1 : x ∈ a), Balanced 𝕜 (b x)) →
      ∃ (j : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) j ∧
          ∀ᶠ (x : α) in l,
            (egauge 𝕜 (E := (i : ι) → E i) (a.pi (α := E) fun (i : ι) ↦ b i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 j (g x)
⊢ IsBigOTVS 𝕜 (E := (i : ι) → E i) l (fun (x : α) (i : ι) ↦ f i x) g

Tactic:
simp only [this.isBigOTVS_iff (basis_sets _), forall_and, Prod.forall, id]

Premises used: id, Filter.basis_sets, Filter.HasBasis.isBigOTVS_iff, Prod.forall, forall_and
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
⊢ ∀ (i : ι) (hi : i ∈ I), ∀ᶠ (V : Set F) in smallSets (𝓝 0), ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)

Tactic:
have := fun i hi ↦ (h i).eventually_smallSets (U i) (hU i hi)
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I), ∀ᶠ (V : Set F) in smallSets (𝓝 0), ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
rcases :
  ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
    (hV : ∀ i ∈ I, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)),
    ∃ (j : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) j ∧
        ∀ᶠ (x : α) in l,
          (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 j (g x)
⊢ ∃ (j : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) j ∧
      ∀ᶠ (x : α) in l,
        (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 j (g x)

Tactic:
rcases (hIf.eventually_all.mpr this).exists_mem_of_smallSets with ⟨V, hV₀, hV⟩

Premises used: Iff.mpr, Set.Finite.eventually_all, Filter.Eventually.exists_mem_of_smallSets
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I), ∀ᶠ (V : Set F) in smallSets (𝓝 0), ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
right :
  ∀ᶠ (x : α) in l,
    (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 V (g x)
⊢ ∃ (j : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) j ∧
      ∀ᶠ (x : α) in l,
        (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 j (g x)

Tactic:
use V, hV₀
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup F
inst_2 : TopologicalSpace F
inst_3 : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst_4 : (i : ι) → AddCommGroup (E i)
inst_5 : (i : ι) → Module.{u_3, u_8} 𝕜 (E i)
inst_6 : (i : ι) → TopologicalSpace (E i)
inst_7 : ∀ (i : ι), ContinuousSMul.{u_3, u_8} 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =O[𝕜; l] g
this_1 :
  HasBasis (α := (i : ι) → E i) (𝓝 0)
    (fun (If : Set ι × ((i : ι) → Set (E i))) ↦
      If.1.Finite ∧ ∀ i ∈ If.1, Membership.mem (γ := Filter (E i)) (𝓝 0) (If.2 i) ∧ Balanced 𝕜 (If.2 i))
    fun (If : Set ι × ((i : ι) → Set (E i))) ↦ If.1.pi (α := E) fun (i : ι) ↦ id (If.2 i)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ (x : ι) (x_1 : x ∈ I), Membership.mem (γ := Filter (E x)) (𝓝 0) (U x)
Ub : ∀ (x : ι) (x_1 : x ∈ I), Balanced 𝕜 (U x)
this :
  ∀ (i : ι) (hi : i ∈ I), ∀ᶠ (V : Set F) in smallSets (𝓝 0), ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : ∀ i ∈ I, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
⊢ ∀ᶠ (x : α) in l,
    (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 V (g x)

Tactic:
(hIf.eventually_all.mpr hV).mono fun x hx ↦ ?_

Premises used: Iff.mpr, Set.Finite.eventually_all, Filter.Eventually.mono