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
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)
ε : ℝ≥0
hε : ε ≠ 0
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * 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 : α) ↦ (↑ε : ℝ≥0∞) * 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 : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)) x))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [hV ε hε, hW] with x hx₁ hx₂ using hx₁.trans <| by gcongr
-- 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)
ε : ℝ≥0
hε : ε ≠ 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ egauge 𝕜 U (f x)) x)
                    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * 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 : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)) x))
                      x}
                  x}
            x}
      a
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
have h₁ : ∀ (a : α),
  egauge 𝕜 U (f a) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g a) →
    egauge 𝕜 V (g a) ≤ egauge 𝕜 W (k a) → egauge 𝕜 U (f a) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k a)
Tactic: filter_upwards [hV ε hε, hW] with x hx₁ hx₂ using hx₁.trans <| by gcongr
-- 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 : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ 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 : l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ 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 :
    ∀ (ε : ℝ≥0),
      ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * 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 : 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 :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * 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ε ↦ ?_⟩
-- 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 :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * 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 : α) ↦ (↑ε : ℝ≥0∞) * 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 : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)) x))
                    x}
                x}
          x}
    a
Tactic: filter_upwards [hV, hW ε hε] 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 :
  ∀ (ε : ℝ≥0),
    ε ≠ 0 → l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 V (g x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
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 : α) ↦ (↑ε : ℝ≥0∞) * 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 : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)) x))
                      x}
                  x}
            x}
      a
⊢ l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k x)
have h₁ : ∀ (a : α),
  egauge 𝕜 U (f a) ≤ egauge 𝕜 V (g a) →
    egauge 𝕜 V (g a) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k a) → egauge 𝕜 U (f a) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 W (k a)
Tactic: filter_upwards [hV, hW ε hε] 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
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : AddCommGroup F
inst_5 : TopologicalSpace F
inst_6 : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
⊢ f =o[𝕜; l] g ↔
    ∀ (i : ιE),
      pE i →
        ∃ (j : ιF),
          pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (sF j) (g x)
have rw : (∀ (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)) ↔
  ∀ (i : ιE),
    pE i →
      ∃ (j : ιF),
        pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (sF j) (g x)
Tactic: rw [isLittleOTVS_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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
⊢ (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (ε : ℝ≥0),
              ε ≠ 0 →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE),
      pE i →
        ∃ (j : ιF),
          pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (sF j) (g x)
have refine_1 : ∀ ⦃s t : Set E⦄,
  s ⊆ t →
    (∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦
                (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)
Tactic: refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
refine_1 :
  ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (ε : ℝ≥0),
              ε ≠ 0 →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            ∀ (ε : ℝ≥0),
              ε ≠ 0 →
                l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (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 (f x)) fun (x : α) ↦
                  (↑ε : ℝ≥0∞) * egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE),
      pE i →
        ∃ (j : ιF),
          pF j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (sF j) (g x)
have refine_2 : ∀ (x : ιE),
  pE x →
    ∀ ⦃s t : Set F⦄,
      s ⊆ t →
        (∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) fun (x : α) ↦
                (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) →
          ∀ (ε : ℝ≥0),
            ε ≠ 0 →
              l.EventuallyLE (β := ℝ≥0∞) (fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) fun (x : α) ↦
                (↑ε : ℝ≥0∞) * egauge 𝕜 s (g x)
Tactic: refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
x : ιE
h : pE x
⊢ ∀ ⦃s t : Set F⦄,
    s ⊆ t →
      (∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦
              (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) →
        ∀ (ε : ℝ≥0),
          ε ≠ 0 →
            l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦
              (↑ε : ℝ≥0∞) * egauge 𝕜 s (g x)
have refine_2 : ∀ (s t : Set F) (hsub : s ⊆ t)
  (h :
    ∀ (ε : ℝ≥0),
      ε ≠ 0 →
        l.EventuallyLE (β := ℝ≥0∞) (fun (x_1 : α) ↦ egauge 𝕜 (sE x) (f x_1)) fun (x : α) ↦
          (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x))
  (ε : ℝ≥0) (hε : ε ≠ 0) (x_1 : α)
  (hx :
    LE.le (α := ℝ≥0∞) ((fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) x_1)
      ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) x_1)),
  LE.le (α := ℝ≥0∞) ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 t (g x)) x_1)
    ((fun (x : α) ↦ (↑ε : ℝ≥0∞) * egauge 𝕜 s (g x)) x_1)
Tactic: refine fun s t hsub h ε hε ↦ (h ε hε).mono fun x hx ↦ hx.trans ?_
-- 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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
⊢ f =O[𝕜; l] g ↔ ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)
have rw : (∀ (U : Set E),
    Membership.mem (γ := Filter E) (𝓝 0) U →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)) ↔
  ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)
Tactic: 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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
⊢ (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)
have refine_1 : ∀ ⦃s t : Set E⦄,
  s ⊆ t →
    (∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)) →
      ∃ (V : Set F),
        Membership.mem (γ := Filter F) (𝓝 0) V ∧
          l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
Tactic: refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_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
ιE : Sort u_7
ιF : Sort u_8
pE : ιE → Prop
pF : ιF → Prop
sE : ιE → Set E
sF : ιF → Set F
hE : HasBasis (𝓝 0) pE sE
hF : HasBasis (𝓝 0) pF sF
refine_1 :
  ∀ ⦃s t : Set E⦄,
    s ⊆ t →
      (∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 s (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)) →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 t (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)
⊢ (∀ (U : Set E),
      Membership.mem (γ := Filter E) (𝓝 0) U →
        ∃ (V : Set F),
          Membership.mem (γ := Filter F) (𝓝 0) V ∧
            l.EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ egauge 𝕜 U (f x)) fun (x : α) ↦ egauge 𝕜 V (g x)) ↔
    ∀ (i : ιE), pE i → ∃ (j : ιF), pF j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (sE i) (f x) ≤ egauge 𝕜 (sF j) (g x)
have refine_2 : ∀ (x : ιE),
  pE x →
    ∀ ⦃s t : Set F⦄,
      s ⊆ t →
        (l.EventuallyLE (β := ℝ≥0∞) (fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) fun (x : α) ↦ egauge 𝕜 t (g x)) →
          l.EventuallyLE (β := ℝ≥0∞) (fun (x_2 : α) ↦ egauge 𝕜 (sE x) (f x_2)) fun (x : α) ↦ egauge 𝕜 s (g x)
Tactic: refine (hE.forall_iff ?_).trans <| forall₂_congr fun _ _ ↦ hF.exists_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
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)
⊢ f =O[𝕜; l] g
have rw : ∀ (i : ι),
  p i →
    ∃ (j : Set F),
      Membership.mem (γ := Filter F) (𝓝 0) j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f x) ≤ egauge 𝕜 (id j) (g x)
Tactic: rw [hb.isBigOTVS_iff (basis_sets _)]