awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
⊢ (∀ (i : ℝ),
      0 < i →
        ∃ (j : ℝ),
          0 < j ∧
            ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ⟨1, one_pos, fun δ hδ ↦ ?_⟩⟩

Premises used: And.intro, Iff.intro, Exists.intro, OfNat.ofNat, one_pos
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
refine_1 :
  ∀
    (h :
      ∀ (i : ℝ),
        0 < i →
          ∃ (j : ℝ),
            0 < j ∧
              ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x))
    (ε : ℝ) (hε : 0 < ε), ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
refine_2 :
  ∀ (h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) (ε : ℝ) (hε : 0 < ε) (δ : ℝ≥0) (hδ : δ ≠ 0),
    ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
⊢ (∀ (i : ℝ),
      0 < i →
        ∃ (j : ℝ),
          0 < j ∧
            ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ⟨1, one_pos, fun δ hδ ↦ ?_⟩⟩
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ
hε : 0 < ε
refine_1 :
  ∀ (δ : ℝ) (hδ₀ : 0 < δ)
    (hδ :
      ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)),
    ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖

Tactic:
rcases h ε hε with ⟨δ, hδ₀, hδ⟩
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)
⊢ 0 ≤ ε

Tactic:
hε.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)
refine_1 :
  ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ))
    (hδ :
      ∀ (ε_1 : ℝ≥0),
        ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)),
    ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖

Tactic:
lift ε to ℝ≥0 using hε.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
δ : ℝ
hδ₀ : 0 < δ
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hδ :
  ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)
⊢ 0 ≤ δ

Tactic:
hδ₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
δ : ℝ
hδ₀ : 0 < δ
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hδ :
  ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)
refine_1 :
  ∀ (δ : ℝ≥0) (hδ₀ : 0 < (↑δ : ℝ))
    (hδ :
      ∀ (ε_1 : ℝ≥0),
        ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)),
    ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖

Tactic:
lift δ to ℝ≥0 using hδ₀.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
δ : ℝ≥0
hδ₀ : 0 < (↑δ : ℝ)
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ 0 < ε

Tactic:
norm_cast at hε hδ₀
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
δ : ℝ≥0
hδ₀ : 0 < (↑δ : ℝ)
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε₁ : 0 < ε
⊢ 0 < δ

Tactic:
norm_cast at hε hδ₀
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
h₁ :
  ∀ (x : α) (hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)),
    ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖

Tactic:
filter_upwards [hδ (δ / ‖c‖₊) (div_pos hδ₀ hc₀).ne'] with x hx

Premises used: NNNorm.nnnorm, HDiv.hDiv, LT.lt.ne', div_pos
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
this : (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
⊢ (↑(‖f x‖₊ / ε) : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
rw [← ENNReal.coe_div hε.ne'] at this

Premises used: LT.lt.ne', ENNReal.coe_div
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
this : (↑(‖f x‖₊ / ε) : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
rw : ‖f x‖ / (↑ε : ℝ) ≤ ‖g x‖
⊢ ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖

Tactic:
rw [← div_le_iff₀' (NNReal.coe_pos.2 hε)]

Premises used: Iff.mpr, NNReal.coe_pos, div_le_iff₀'
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
this : (↑(‖f x‖₊ / ε) : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
⊢ ‖f x‖ / (↑ε : ℝ) ≤ ‖g x‖

Tactic:
exact_mod_cast this
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
h₁ : (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
⊢ ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖

Tactic:
suffices (‖f x‖₊ / ε : ℝ≥0∞) ≤ ‖g x‖₊ by
      rw [← ENNReal.coe_div hε.ne'] at this
      rw [← div_le_iff₀' (NNReal.coe_pos.2 hε)]
      exact_mod_cast this
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x)

Tactic:
div_le_egauge_ball 𝕜 _ _

Premises used: div_le_egauge_ball
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)

Tactic:
hx
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
h₁ : (↑(δ / ‖c‖₊) : ℝ≥0∞) ≤ (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)
h₂ : egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤ (↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞)
⊢ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤
    (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑(δ / ‖c‖₊) : ℝ≥0∞) ≤ (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)

Tactic:
ENNReal.coe_div_le

Premises used: ENNReal.coe_div_le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤ (↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞)

Tactic:
egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)

Premises used: egauge_ball_le_of_one_lt_norm, ne_of_gt, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑(δ / ‖c‖₊) : ℝ≥0∞) ≤ (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)

Tactic:
exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]

Premises used: egauge_ball_le_of_one_lt_norm, ne_of_gt, Or.inl, ENNReal.coe_div_le
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑δ : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞)⁻¹ * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) * (↑δ : ℝ≥0∞)⁻¹) =
    (↑δ : ℝ≥0∞) * (↑δ : ℝ≥0∞)⁻¹ * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞)⁻¹) * (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
ring
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
bc : (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) ≤ 1
bc₁ : (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) ≤ 1
⊢ (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) ≤ 1

Tactic:
ENNReal.div_self_le_one

Premises used: ENNReal.div_self_le_one
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) ≤ 1

Tactic:
exact ENNReal.div_self_le_one

Premises used: ENNReal.div_self_le_one
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) ≤ 1

Tactic:
ENNReal.div_self_le_one

Premises used: ENNReal.div_self_le_one
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) ≤ 1

Tactic:
exact ENNReal.div_self_le_one

Premises used: ENNReal.div_self_le_one
-- Module: Mathlib.Analysis.Asymptotics.TVS
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞) = (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
simp