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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
hε : Ne (α := ℝ≥0∞) ∞ 0
x : α
⊢ 1 * egauge 𝕜 V (g x) ≤ ∞ * egauge 𝕜 V (g x)
have grw : 1 * egauge 𝕜 V (g x) ≤ 1 * egauge 𝕜 V (g x)
Tactic: grw [← le_top]
-- 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
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
hε : Ne (α := ℝ≥0∞) ∞ 0
x : α
grw : 1 * egauge 𝕜 V (g x) ≤ 1 * egauge 𝕜 V (g x)
⊢ 1 * egauge 𝕜 V (g x) ≤ ∞ * egauge 𝕜 V (g x)
have grw₁ : ℝ≥0∞
Tactic: grw [← le_top]
-- 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
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)
have top : ∀ (hε : Ne (α := ℝ≥0∞) ∞ 0),
  l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ∞ * egauge 𝕜 V (g x)
Tactic: cases ε with
  | top => exact (hV 1 one_ne_zero).trans <| .of_forall fun _ ↦ by dsimp; grw [← le_top]
  | coe ε => exact hV ε (mod_cast hε)
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
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
ε : ℝ≥0∞
hε : ε ≠ 0
top :
  ∀ (hε : Ne (α := ℝ≥0∞) ∞ 0),
    l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ∞ * egauge 𝕜 V (g x)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ ε * egauge 𝕜 V (g x)
have coe : ∀ (ε : ℝ≥0) (hε : (↑ε : ℝ≥0∞) ≠ 0),
  l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
Tactic: cases ε with
  | top => exact (hV 1 one_ne_zero).trans <| .of_forall fun _ ↦ by dsimp; grw [← le_top]
  | coe ε => exact hV ε (mod_cast hε)
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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =o[𝕜; l] g₁ ↔ f₂ =o[𝕜; l] g₂
have simp : (∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x) / egauge 𝕜 V (g₁ x)) l (𝓝 0)) ↔
  ∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x) / egauge 𝕜 V (g₂ x)) l (𝓝 0)
Tactic: simp only [isLittleOTVS_iff_tendsto_div]
-- 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₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x) / egauge 𝕜 V (g₁ x)) l (𝓝 0)) ↔
    ∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x) / egauge 𝕜 V (g₂ x)) l (𝓝 0)
have h : ∀ (U : Set E) (hU : Membership.mem (γ := Filter E) (𝓝 0) U) (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V),
  Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x) / egauge 𝕜 V (g₁ x)) l (𝓝 0) ↔
    Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x) / egauge 𝕜 V (g₂ x)) l (𝓝 0)
Tactic: peel with U hU 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
f₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =O[𝕜; l] g₁ ↔ f₂ =O[𝕜; l] g₂
have simp : (∀ (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)) ↔
  ∀ (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)
Tactic: simp only [isBigOTVS_iff]
-- 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₁ f₂ : α → E
g₁ g₂ : α → F
l : Filter α
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ (∀ (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)) ↔
    ∀ (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)
have h : ∀ (U : Set E) (hU : Membership.mem (γ := Filter E) (𝓝 0) U) (V : Set F) (hV : Membership.mem (γ := Filter F) (𝓝 0) V),
  (l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₁ x)) fun (x : α) ↦ egauge 𝕜 V (g₁ x)) ↔
    l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f₂ x)) fun (x : α) ↦ egauge 𝕜 V (g₂ x)
Tactic: peel with U hU V hV
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
f : α → E
l : Filter α
⊢ f =O[𝕜; l] f
have rw : ∀ (U : Set E),
  Membership.mem (γ := Filter E) (𝓝 0) U →
    ∃ (V : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) V ∧
        l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (f x)
Tactic: rw [isBigOTVS_iff]
-- 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
⊢ f =O[𝕜; l] g
have refine : ∀ (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 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
l : Filter α
f : α → E
g : α → F
h : f =o[𝕜; l] g
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 x)
have rcases : ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
  (hV :
    ∀ (ε : ℝ≥0),
      ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)),
  ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
Tactic: rcases h.1 U hU with ⟨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
h : f =o[𝕜; l] g
U : Set E
hU : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∃ (V : Set F),
    Membership.mem (γ := Filter F) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
have right : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (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
E : Type u_4
F : Type u_5
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
⊢ f =O[𝕜; l] k
have refine : ∀ (U : Set E) (hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U),
  ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k 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
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)
have obtain : ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
  (hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)),
  ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)
Tactic: obtain ⟨V, hV₀, hV⟩ := hfg.1 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
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)
have obtain : ∀ (W : Set G) (hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W)
  (hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)),
  ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)
Tactic: obtain ⟨W, hW₀, hW⟩ := hgk.1 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
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (k x)
have refine : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 W (k x)
Tactic: refine ⟨W, hW₀, ?_⟩
-- 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
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 W (k x)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦ LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x) ((fun (x : α) ↦ egauge 𝕜 V (g x)) x))
              x}
          x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α)
                {x : α |
                  (fun (x : α) ↦
                      LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 V (g x)) x) ((fun (x : α) ↦ egauge 𝕜 W (k x)) x))
                    x}
                x →
              Membership.mem (γ := Set α)
                {x : α |
                  (fun (x : α) ↦
                      LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x) ((fun (x : α) ↦ egauge 𝕜 W (k x)) x))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [hV, hW] with x hx₁ hx₂ using hx₁.trans 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
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x) ((fun (x : α) ↦ egauge 𝕜 V (g x)) x))
                x}
            x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 V (g x)) x) ((fun (x : α) ↦ egauge 𝕜 W (k x)) x))
                      x}
                  x →
                Membership.mem (γ := Set α)
                  {x : α |
                    (fun (x : α) ↦
                        LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x) ((fun (x : α) ↦ egauge 𝕜 W (k x)) x))
                      x}
                  x}
            x}
      a
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 W (k x)
have h₁ : ∀ (a : α),
  egauge 𝕜 U (f a) ≤ egauge 𝕜 V (g a) → egauge 𝕜 V (g a) ≤ egauge 𝕜 W (k a) → egauge 𝕜 U (f a) ≤ egauge 𝕜 W (k a)
Tactic: filter_upwards [hV, hW] with x hx₁ hx₂ using hx₁.trans 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
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
⊢ f =o[𝕜; l] k
have refine : ∀ (U : Set E) (hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U),
  ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
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
G : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
inst_7 : AddCommGroup G
inst_8 : TopologicalSpace G
inst_9 : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
have obtain : ∀ (V : Set F) (hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V)
  (hV :
    ∀ (ε : ℝ≥0),
      ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)),
  ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
Tactic: obtain ⟨V, hV₀, hV⟩ := hfg.1 U hU₀
-- 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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
have obtain : ∀ (W : Set G) (hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W)
  (hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)),
  ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
Tactic: obtain ⟨W, hW₀, hW⟩ := hgk.1 V hV₀
-- 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
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
V : Set F
hV₀ : Membership.mem (γ := Filter F) (𝓝 0) V
hV :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
W : Set G
hW₀ : Membership.mem (γ := Filter G) (𝓝 0) W
hW : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ egauge 𝕜 W (k x)
⊢ ∃ (V : Set G),
    Membership.mem (γ := Filter G) (𝓝 0) V ∧
      ∀ (ε : ℝ≥0),
        ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (k x)
have refine : ∀ (ε : ℝ≥0) (hε : ε ≠ 0),
  l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
Tactic: refine ⟨W, hW₀, fun ε hε ↦ ?_⟩