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‖₊
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∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤
    (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞))
ε₂ :
  (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞)) =
    (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞)
ε₃ :
  (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞)
ε₄ : HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞) = (↑‖g x‖₊ : ℝ≥0∞)
⊢ (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
calc
      (‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
      _ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
      _ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
      _ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
      _ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = ‖g x‖₊ := by simp

Premises used: ENNReal.ofNNReal, HMul.hMul, NNNorm.nnnorm, HDiv.hDiv, Metric.ball, div_le_egauge_ball, OfNat.ofNat, egauge, NNReal.toReal
-- 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
⊢ 0 < ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ)

Tactic:
positivity
-- 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
x : α
h₁ :
  ∀ (hx : (↑‖f x‖₊ : ℝ) ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)),
    egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
⊢ ‖f x‖ ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * ‖g x‖ → egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)

Tactic:
(hx : ‖f x‖₊ ≤ ε * δ / ‖c‖₊ * ‖g x‖₊)
-- 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
h₁ :
  ∀ (x : α) (hx : (↑‖f x‖₊ : ℝ) ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)),
    egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)

Tactic:
filter_upwards [@h ↑(ε * δ / ‖c‖₊) (by positivity)] with x (hx : ‖f x‖₊ ≤ ε * δ / ‖c‖₊ * ‖g x‖₊)
-- 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
x : α
hx : (↑‖f x‖₊ : ℝ) ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
x : α
hx : (↑‖f x‖₊ : ℝ) ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
h₁ :
  ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ)) (hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)),
    egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
⊢ egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑‖c‖₊ : ℝ≥0∞) * (↑‖f 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
hab : (↑‖f x‖₊ : ℝ≥0∞) ≤ (↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
⊢ (↑‖c‖₊ : ℝ≥0∞) * (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ (↑‖f x‖₊ : ℝ≥0∞) ≤ (↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
exact_mod_cast 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
simp :
  (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) * (↑δ : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞)⁻¹ * (↑‖g x‖₊ : ℝ≥0∞)) * (↑ε : ℝ≥0∞)⁻¹ =
    (↑‖c‖₊ : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞)⁻¹ * ((↑ε : ℝ≥0∞) * (↑ε : ℝ≥0∞)⁻¹) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
⊢ (↑‖c‖₊ : ℝ≥0∞) * ((↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)) / (↑ε : ℝ≥0∞) =
    (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
simp only [div_eq_mul_inv, ENNReal.coe_inv hc₀.ne', ENNReal.coe_mul]

Premises used: ENNReal.coe_inv, div_eq_mul_inv, LT.lt.ne', ENNReal.coe_mul
-- 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) * (↑δ : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞)⁻¹ * (↑‖g x‖₊ : ℝ≥0∞)) * (↑ε : ℝ≥0∞)⁻¹ =
    (↑‖c‖₊ : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞)⁻¹ * ((↑ε : ℝ≥0∞) * (↑ε : ℝ≥0∞)⁻¹) * (↑δ : ℝ≥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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
bc : (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) ≤ 1
bc₁ : (↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ 1
⊢ (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑δ : ℝ≥0∞) * (↑‖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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ HMul.hMul (α := ℝ≥0∞) 1 1 * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) = (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)

Tactic:
simp
-- 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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
bc : (↑‖g x‖₊ : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 1) (g x)
⊢ (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)

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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ (↑‖g x‖₊ : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 1) (g x)

Tactic:
apply le_egauge_ball_one

Premises used: le_egauge_ball_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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
egauge :
  (↑‖c‖₊ : ℝ≥0∞) * (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤
    (↑‖c‖₊ : ℝ≥0∞) * ((↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)) / (↑ε : ℝ≥0∞)
egauge₁ :
  (↑‖c‖₊ : ℝ≥0∞) * ((↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)) / (↑ε : ℝ≥0∞) =
    (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
egauge₂ :
  (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
egauge₃ : HMul.hMul (α := ℝ≥0∞) 1 1 * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) = (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
egauge₄ : (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤ (↑δ : ℝ≥0∞) * _root_.egauge 𝕜 (ball 0 1) (g x)
⊢ _root_.egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑δ : ℝ≥0∞) * _root_.egauge 𝕜 (ball 0 1) (g x)

Tactic:
calc
      egauge 𝕜 (ball 0 ε) (f x) ≤ ‖c‖₊ * ‖f x‖₊ / ε :=
        egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hε)
      _ ≤ ‖c‖₊ * (↑(ε * δ / ‖c‖₊) * ‖g x‖₊) / ε := by gcongr; exact_mod_cast hx
      _ = (‖c‖₊ / ‖c‖₊) * (ε / ε) * δ * ‖g x‖₊ := by
        simp only [div_eq_mul_inv, ENNReal.coe_inv hc₀.ne', ENNReal.coe_mul]; ring
      _ ≤ 1 * 1 * δ * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = δ * ‖g x‖₊ := by simp
      _ ≤ δ * egauge 𝕜 (ball 0 1) (g x) := by gcongr; apply le_egauge_ball_one

Premises used: egauge_ball_le_of_one_lt_norm, HMul.hMul, NNNorm.nnnorm, ne_of_gt, HDiv.hDiv, Metric.ball, Or.inl, OfNat.ofNat, egauge, NNReal.toReal
-- 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 α
rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖₊), f =O[𝕜; l] g ↔ f =O[l] g
⊢ f =O[𝕜; l] g ↔ f =O[l] g

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc : 1 < ‖c‖₊⟩

Premises used: NormedField.exists_one_lt_norm
-- 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‖₊
mp : f =O[𝕜; l] g → f =O[l] g
mpr : f =O[l] g → f =O[𝕜; l] g
⊢ f =O[𝕜; l] g ↔ f =O[l] g

Tactic:
constructor
-- 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‖₊
mp :
  (∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)) →
    ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[𝕜; l] g → f =O[l] g

Tactic:
rw [nhds_basis_ball.isBigOTVS_iff nhds_basis_ball, isBigO_iff]

Premises used: Asymptotics.isBigO_iff, Filter.HasBasis.isBigOTVS_iff, Metric.nhds_basis_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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
mp :
  ∀ (r : ℝ) (hr₀ : 0 < r) (hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 r) (g x)),
    ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rcases h 1 one_pos with ⟨r, hr₀, hr⟩

Premises used: 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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ
hr₀ : 0 < r
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 r) (g x)
⊢ 0 ≤ r

Tactic:
hr₀.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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ
hr₀ : 0 < r
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 r) (g x)
mp :
  ∀ (r : ℝ≥0) (hr₀ : 0 < (↑r : ℝ)) (hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)),
    ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
lift r to ℝ≥0 using hr₀.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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr₀ : 0 < (↑r : ℝ)
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
⊢ 0 < r

Tactic:
norm_cast at hr₀
-- 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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
⟨(‖c‖₊ / r : ℝ≥0), hr.mono fun x hx ↦ ?_⟩

Premises used: NNNorm.nnnorm, HDiv.hDiv, Filter.Eventually.mono, Exists.intro, NNReal.toReal
-- 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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
mp : ∀ (x : α) (hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)), ‖f x‖ ≤ (↑(‖c‖₊ / r) : ℝ) * ‖g x‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
refine ⟨(‖c‖₊ / r : ℝ≥0), hr.mono fun x 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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
this : ‖f x‖ₑ ≤ (↑(‖c‖₊ / r) : ℝ≥0∞) * ‖g x‖ₑ
simp : (↑‖f x‖₊ : ℝ) ≤ (↑(‖c‖₊ / r) : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ ‖f x‖ ≤ (↑(‖c‖₊ / r) : ℝ) * ‖g x‖

Tactic:
simp only [enorm_eq_nnnorm, ← coe_nnnorm] at this ⊢

Premises used: enorm_eq_nnnorm, coe_nnnorm
-- 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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
this : (↑‖f x‖₊ : ℝ≥0∞) ≤ (↑(‖c‖₊ / r) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
⊢ (↑‖f x‖₊ : ℝ) ≤ (↑(‖c‖₊ / r) : ℝ) * (↑‖g x‖₊ : ℝ)

Tactic:
mod_cast this

Premises used: NNReal.coe_le_coe._simp_1, cast, ENNReal.coe_le_coe._simp_1, Eq.symm, NNReal.toReal, Eq.trans
-- 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‖₊
h : ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
r : ℝ≥0
hr : ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
hr₀ : 0 < r
x : α
hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)
this : (↑‖f x‖₊ : ℝ≥0∞) ≤ (↑(‖c‖₊ / r) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
⊢ (↑‖f x‖₊ : ℝ) ≤ (↑(‖c‖₊ / r) : ℝ) * (↑‖g x‖₊ : ℝ)

Tactic:
exact mod_cast this