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
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
⊢ ∃ (j : Set F), Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
have 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)
Tactic: rcases h i hi with ⟨C, V, hV₀, hV⟩
-- 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
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)
⊢ ∃ (j : Set F), Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
have 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)
Tactic: rcases NormedField.exists_lt_nnnorm 𝕜 C with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
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‖₊
⊢ ∃ (j : Set F), Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
have hc₀ : c ≠ 0
Tactic: have hc₀ : c ≠ 0 := by rintro rfl; simp at hc
-- 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
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)
have refine : ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)
Tactic: refine ⟨c⁻¹ • V, (set_smul_mem_nhds_zero_iff <| inv_ne_zero hc₀).mpr hV₀, ?_⟩
-- 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
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)
have refine : ∀ (x : α),
  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑C : ℝ≥0∞) * egauge 𝕜 V (g x)) x) ((fun (x : α) ↦ egauge 𝕜 (id (c⁻¹ • V)) (g x)) x)
Tactic: refine hV.trans <| .of_forall fun x ↦ ?_
-- 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
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)
have grw : (↑‖c‖₊ : ℝ≥0∞) * egauge 𝕜 V (g x) ≤ egauge 𝕜 (id (c⁻¹ • V)) (g x)
Tactic: grw [hc]
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
⊢ IsBigOTVS.{u_3, u_1, u_4, u_5} 𝕜 (F := F) l f ((⇑g : (a : E) → F) ∘ f)
have exists_eventuallyLE : ∀ (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 : (a : E) → F) ∘ f) x)
Tactic: constructor
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)
have exists_eventuallyLE : ∀ (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V) (hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U),
  ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)
Tactic: rcases mem_comap.1 (hg hU) with ⟨V, hV, hgV⟩
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)
have right : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)
Tactic: use V, hV
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) x)
have right : ∀ (a : α), egauge 𝕜 U (f a) ≤ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) a)
Tactic: filter_upwards with a
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
⊢ egauge 𝕜 U (f a) ≤ egauge 𝕜 V (((⇑g : (a : E) → F) ∘ f) a)
have right : ∀ (c : 𝕜) (hc₀ : c ≠ 0) (hc : ((⇑g : (a : E) → F) ∘ f) a ∈ c • V), egauge 𝕜 U (f a) ≤ ‖c‖ₑ
Tactic: refine le_egauge_of_forall_ne_zero (mem_of_mem_nhds hV) fun c hc₀ hc ↦ ?_
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : ((⇑g : (a : E) → F) ∘ f) a ∈ c • V
⊢ egauge 𝕜 U (f a) ≤ ‖c‖ₑ
have right : f a ∈ c • U
Tactic: apply egauge_le_of_mem_smul
-- 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 : E →ₗ[𝕜] F
hg : LE.le.{u_4} (α := Filter E) (comap.{u_4, u_5} (β := F) (⇑g : (a : E) → F) (𝓝 0)) (𝓝 0)
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV : Membership.mem (γ := Filter F) (𝓝 0) V
hgV : (⇑g : (a : E) → F) ⁻¹' V ⊆ U
a : α
c : 𝕜
hc₀ : c ≠ 0
hc : ((⇑g : (a : E) → F) ∘ f) a ∈ c • V
⊢ f a ∈ c • U
have right : Membership.mem (γ := Set E) ((⇑g : (a : E) → F) ⁻¹' (c • V)) (f a)
Tactic: grw [← hgV, ← (IsUnit.mk0 _ hc₀).preimage_smul_set]
-- 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
g : α → F
l : Filter α
⊢ IsLittleOTVS.{u_3, u_1, u_4, u_5} 𝕜 (E := E) l 0 g
have refine : ∀ (U : Set E) (hU : Membership.mem (γ := Filter E) (𝓝 0) U),
  ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (0 x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
Tactic: refine ⟨fun U hU ↦ ?_⟩
-- 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
g : α → F
l : Filter α
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (0 x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
have h : Membership.mem (γ := Filter F) (𝓝 0) univ ∧
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (0 x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 univ (g x)
Tactic: use univ
-- 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
f : α → E
g : α → F
inst_7 : TopologicalSpace α
x : α
s : Set α
h : f x = 0
⊢ f =o[𝕜; 𝓝[insert x s] x] g ↔ f =o[𝕜; 𝓝[s] x] g
have rw : f =o[𝕜; pure x] g
Tactic: rw [nhdsWithin_insert, isLittleOTVS_sup, and_iff_right]
-- 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
⊢ IsLittleOTVS 𝕜 (E := E × F) l (fun (x : α) ↦ (f x, g x)) k
have rw : ∀ (i : Prod.{u_4, u_5} (Set E) (Set F)),
  (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
      Membership.mem (γ := Filter F) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2 →
    ∃ (j : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) j ∧
        ∀ (ε : ℝ≥0),
          ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id j) (k x)
Tactic: rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isLittleOTVS_iff
    (basis_sets _)]
-- 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
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id j) (k x)
have rcases : ∀ (W : Set G) (hW : Membership.mem (γ := Filter G) (𝓝 0) W)
  (hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x))
  (hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)),
  ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id j) (k x)
Tactic: rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets
    with ⟨W, hW, hWf, hWg⟩
-- 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 : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id j) (k x)
have refine : ∀ (ε : ℝ≥0) (hε : ε ≠ 0),
  ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id W) (k x)
Tactic: refine ⟨W, hW, fun ε 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
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 : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id W) (k x)
have h : ∀ (x : α) (hfx : egauge 𝕜 U (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x))
  (hgx : egauge 𝕜 V (g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)),
  egauge 𝕜 (id U ×ˢ id V) (f x, g x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (id W) (k x)
Tactic: filter_upwards [hWf ε hε, hWg ε hε] with x hfx hgx
-- 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
⊢ IsBigOTVS 𝕜 (E := E × F) l (fun (x : α) ↦ (f x, g x)) k
have rw : ∀ (i : Prod.{u_4, u_5} (Set E) (Set F)),
  (Membership.mem (γ := Filter E) (𝓝 0) i.1 ∧ Balanced 𝕜 i.1) ∧
      Membership.mem (γ := Filter F) (𝓝 0) i.2 ∧ Balanced 𝕜 i.2 →
    ∃ (j : Set G),
      Membership.mem (γ := Filter G) (𝓝 0) j ∧
        ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
Tactic: rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isBigOTVS_iff (basis_sets _)]
-- 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
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
have rcases : ∀ (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)),
  ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
Tactic: rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets
    with ⟨W, hW, hWf, hWg⟩
-- 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)
⊢ ∃ (j : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) j ∧
      ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
have refine : ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id W) (k x)
Tactic: refine ⟨W, hW, ?_⟩