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 : 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
⊢ (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
have bc₁ : (↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ 1
Tactic: 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
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∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
have bc : (↑‖g x‖₊ : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 1) (g x)
Tactic: 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
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) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
have egauge : (↑‖c‖₊ : ℝ≥0∞) * (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤
  (↑‖c‖₊ : ℝ≥0∞) * ((↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)) / (↑ε : ℝ≥0∞)
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
-- 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 : 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∞)
⊢ _root_.egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑δ : ℝ≥0∞) * _root_.egauge 𝕜 (ball 0 1) (g x)
have egauge₁ : (↑‖c‖₊ : ℝ≥0∞) * ((↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)) / (↑ε : ℝ≥0∞) =
  (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
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
-- 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 : 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∞)
⊢ _root_.egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑δ : ℝ≥0∞) * _root_.egauge 𝕜 (ball 0 1) (g x)
have egauge₂ : (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤
  HMul.hMul (α := ℝ≥0∞) 1 1 * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
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
-- 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 : 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∞)
⊢ _root_.egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑δ : ℝ≥0∞) * _root_.egauge 𝕜 (ball 0 1) (g x)
have egauge₃ : HMul.hMul (α := ℝ≥0∞) 1 1 * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) = (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
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
-- 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 : 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∞)
⊢ _root_.egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑δ : ℝ≥0∞) * _root_.egauge 𝕜 (ball 0 1) (g x)
have egauge₄ : (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤ (↑δ : ℝ≥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
-- 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 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
⊢ f =O[𝕜; l] g ↔ f =O[l] g
have rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖₊), f =O[𝕜; l] g ↔ f =O[l] g
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc : 1 < ‖c‖₊⟩
-- 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 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
⊢ f =O[𝕜; l] g ↔ f =O[l] g
have mp : f =O[𝕜; l] g → f =O[l] g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : 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
⊢ f =O[𝕜; l] g ↔ f =O[l] g
have mpr : f =O[l] g → f =O[𝕜; l] g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
⊢ f =O[𝕜; l] g → f =O[l] g
have 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‖
Tactic: rw [nhds_basis_ball.isBigOTVS_iff nhds_basis_ball, isBigO_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 : 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)
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have 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‖
Tactic: rcases h 1 one_pos with ⟨r, hr₀, hr⟩
-- 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 : 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)
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have 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‖
Tactic: lift r to ℝ≥0 using hr₀.le
Cleared hypotheses: r, hr₀, hr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : 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)
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have hr₁ : 0 < r
Tactic: norm_cast at hr₀
Cleared hypotheses: hr₀
-- 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 : 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‖
have mp : ∀ (x : α) (hx : egauge 𝕜 (ball 0 1) (f x) ≤ egauge 𝕜 (ball 0 (↑r : ℝ)) (g x)), ‖f x‖ ≤ (↑(‖c‖₊ / r) : ℝ) * ‖g x‖
Tactic: refine ⟨(‖c‖₊ / r : ℝ≥0), hr.mono fun x 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 : 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‖ₑ
⊢ ‖f x‖ ≤ (↑(‖c‖₊ / r) : ℝ) * ‖g x‖
have simp : (↑‖f x‖₊ : ℝ) ≤ (↑(‖c‖₊ / r) : ℝ) * (↑‖g x‖₊ : ℝ)
Tactic: simp only [enorm_eq_nnnorm, ← coe_nnnorm] at this ⊢
-- 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 : 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)
⊢ ‖f x‖ ≤ (↑(‖c‖₊ / r) : ℝ) * ‖g x‖
have mp : ‖f x‖ₑ ≤ (↑(‖c‖₊ / r) : ℝ≥0∞) * ‖g x‖ₑ
Tactic: suffices ‖f x‖ₑ ≤ (‖c‖₊ / r : ℝ≥0) * ‖g x‖ₑ by
      simp only [enorm_eq_nnnorm, ← coe_nnnorm] at this ⊢
      exact mod_cast this
-- 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 : 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)
⊢ ‖f x‖ₑ ≤ (↑(‖c‖₊ / r) : ℝ≥0∞) * ‖g x‖ₑ
have egauge : ‖c‖ₑ * ‖g x‖ₑ / (↑r : ℝ≥0∞) = (↑(‖c‖₊ / r) : ℝ≥0∞) * ‖g x‖ₑ
Tactic: calc
      ‖f x‖ₑ ≤ egauge 𝕜 (ball 0 1) (f x) := le_egauge_ball_one ..
      _ ≤ egauge 𝕜 (ball 0 r) (g x) := hx
      _ ≤ ‖c‖ₑ * ‖g x‖ₑ / ↑r :=
        egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'
      _ = (‖c‖₊ / r : ℝ≥0) * ‖g x‖ₑ := by
        simp [hr₀.ne', ENNReal.mul_div_right_comm, enorm_eq_nnnorm]
-- 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 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
⊢ f =O[l] g → f =O[𝕜; l] g
have mpr : (∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
  ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
Tactic: rw [nhds_basis_ball.isBigOTVS_iff nhds_basis_ball, isBigO_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
⊢ (∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ (i : ℝ), 0 < i → ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
have hc₀ : 0 < ‖c‖₊
Tactic: have hc₀ : 0 < ‖c‖₊ := one_pos.trans hc
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : 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‖₊
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
r : ℝ
hr₀ : 0 < r
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
have mpr : ∀ (C : ℝ≥0) (hC₀ : (↑C : ℝ) > 0) (hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖),
  ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
Tactic: lift C to ℝ≥0 using hC₀.le
Cleared hypotheses: C, hC₀, hC
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : 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‖₊
r : ℝ
hr₀ : 0 < r
C : ℝ≥0
hC₀ : (↑C : ℝ) > 0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
have hC₁ : 0 < C
Tactic: norm_cast at hC₀
Cleared hypotheses: hC₀
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : 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‖₊
r : ℝ
hr₀ : 0 < r
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
have mpr : ∀ (r : ℝ≥0) (hr₀ : 0 < (↑r : ℝ)),
  ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
Tactic: lift r to ℝ≥0 using hr₀.le
Cleared hypotheses: r, hr₀
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : 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‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < (↑r : ℝ)
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
have hr₁ : 0 < r
Tactic: norm_cast at hr₀
Cleared hypotheses: hr₀
-- 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 : 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‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
⊢ ∃ (j : ℝ), 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)
have mpr : ∀ (x : α) (hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖),
  egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ egauge 𝕜 (ball 0 ((↑r : ℝ) / ((↑C : ℝ) * (↑‖c‖₊ : ℝ)))) (g x)
Tactic: refine ⟨r / (C * ‖c‖₊), by positivity, hC.mono fun x 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 : 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‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
⊢ ‖c‖ₑ * ‖f x‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞)
have hab : ‖f x‖ₑ ≤ (↑C : ℝ≥0∞) * ‖g x‖ₑ
Tactic: 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
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‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
⊢ ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞) = ‖g x‖ₑ / (↑(r / (C * ‖c‖₊)) : ℝ≥0∞)
have simp_all : ∀ (hc₀ : ¬c = 0) (hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖) (hC₀ : ¬C = 0) (hr₀ : ¬r = 0)
  (hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖),
  (↑r : ℝ≥0∞)⁻¹ * (‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ)) = (↑C : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞) * (↑r : ℝ≥0∞)⁻¹ * ‖g x‖ₑ
Tactic: simp_all [pos_iff_ne_zero, ENNReal.div_eq_inv_mul, ENNReal.mul_inv]
Cleared hypotheses: hc₀, hC, hC₀, hr₀, 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 : 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‖₊
C : ℝ≥0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
hC₀ : 0 < C
r : ℝ≥0
hr₀ : 0 < r
x : α
hx : ‖f x‖ ≤ (↑C : ℝ) * ‖g x‖
⊢ egauge 𝕜 (ball 0 (↑r : ℝ)) (f x) ≤ egauge 𝕜 (ball 0 ((↑r : ℝ) / ((↑C : ℝ) * (↑‖c‖₊ : ℝ)))) (g x)
have egauge : ‖c‖ₑ * ‖f x‖ₑ / (↑r : ℝ≥0∞) ≤ ‖c‖ₑ * ((↑C : ℝ≥0∞) * ‖g x‖ₑ) / (↑r : ℝ≥0∞)
Tactic: calc
      egauge 𝕜 (ball 0 r) (f x) ≤ ‖c‖ₑ * ‖f x‖ₑ / r :=
        egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'
      _ ≤ ‖c‖ₑ * (C * ‖g x‖ₑ) / r := by
        gcongr
        simp only [enorm_eq_nnnorm, ← coe_nnnorm] at hx ⊢
        exact mod_cast hx
      _ = ‖g x‖ₑ / (r / (C * ‖c‖₊) : ℝ≥0) := by
        simp_all [pos_iff_ne_zero, ENNReal.div_eq_inv_mul, ENNReal.mul_inv]
        ac_rfl
      _ ≤ _ := div_le_egauge_ball _ _ _