awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst_10 : ContinuousSMul 𝕜 E
inst_11 : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : Membership.mem (γ := Filter E) (𝓝 0) (U, V).1
hUb : Balanced 𝕜 (U, V).1
hV : Membership.mem (γ := Filter F) (𝓝 0) (U, V).2
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : Membership.mem (γ := Filter G) (𝓝 0) W
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id W) (k x)
have h : ∀ (x : α) (hfx : egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)) (hgx : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)),
  egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ egauge 𝕜 (id W) (k x)
Tactic: filter_upwards [hWf, hWg] with x hfx hgx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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
⊢ IsLittleOTVS 𝕜 (E := (i : ι) → E i) l (fun (x : α) (i : ι) ↦ f i x) g
have 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)
Tactic: have := hasBasis_pi fun i ↦ nhds_basis_balanced 𝕜 (E i)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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)
⊢ IsLittleOTVS 𝕜 (E := (i : ι) → E i) l (fun (x : α) (i : ι) ↦ f i x) g
have 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)
Tactic: rw [← nhds_pi, ← Pi.zero_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ IsLittleOTVS 𝕜 (E := (i : ι) → E i) l (fun (x : α) (i : ι) ↦ f i x) g
have 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)
Tactic: simp only [this.isLittleOTVS_iff (basis_sets _), forall_and, Prod.forall, id]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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)
⊢ ∃ (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)
have 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)
Tactic: have := fun i hi ↦ (h i).eventually_smallSets (U i) (hU i hi)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases (hIf.eventually_all.mpr this).exists_mem_of_smallSets with ⟨V, hV₀, hV⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
have 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)
Tactic: refine ⟨V, hV₀, fun ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
have 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)
Tactic: refine (hIf.eventually_all.mpr (hV · · ε hε)).mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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
⊢ IsBigOTVS 𝕜 (E := (i : ι) → E i) l (fun (x : α) (i : ι) ↦ f i x) g
have 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)
Tactic: have := hasBasis_pi fun i ↦ nhds_basis_balanced 𝕜 (E i)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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)
⊢ IsBigOTVS 𝕜 (E := (i : ι) → E i) l (fun (x : α) (i : ι) ↦ f i x) g
have 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)
Tactic: rw [← nhds_pi, ← Pi.zero_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ IsBigOTVS 𝕜 (E := (i : ι) → E i) l (fun (x : α) (i : ι) ↦ f i x) g
have 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)
Tactic: simp only [this.isBigOTVS_iff (basis_sets _), forall_and, Prod.forall, id]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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)
⊢ ∃ (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)
have this₁ : ∀ (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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases (hIf.eventually_all.mpr this).exists_mem_of_smallSets with ⟨V, hV₀, hV⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use V, hV₀
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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)
have right : ∀ (x : α) (hx : ∀ i ∈ I, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)),
  (egauge 𝕜 (E := (i : ι) → E i) (I.pi (α := E) fun (i : ι) ↦ U i) fun (i : ι) ↦ f i x) ≤ egauge 𝕜 V (g x)
Tactic: refine (hIf.eventually_all.mpr hV).mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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
c : α → 𝕜
⊢ IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) (F := F) l (fun (x : α) ↦ c x • f x) fun (x : α) ↦ c x • g x
have simp : ∀
  (h :
    ∀ (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))
  (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 (c x • f x)) fun (x : α) ↦
              (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)
Tactic: simp only [isLittleOTVS_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
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
c : α → 𝕜
h :
  ∀ (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)
⊢ ∀ (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 (c x • f x)) fun (x : α) ↦
                (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)
have h₁ : ∀ (U : Set E) (hU : Membership.mem (γ := Filter E) (𝓝 0) U) (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V)
  (ε : ℝ≥0) (hε : ε ≠ 0) (x : α)
  (hx : LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) x)),
  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (c x • f x)) x) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (c x • g x)) x)
Tactic: peel h with U hU V hV ε hε x hx