case intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : IsBigOWith C cofinite f g''
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
rcases h.exists_pos with ⟨C, C₀, hC⟩
case intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
case intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : IsBigOWith C cofinite f g''
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
rw [IsBigOWith_def, eventually_cofinite] at hC
case intro.intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
case intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
rcases (hC.toFinset.image fun x => ‖f x‖ / ‖g'' x‖).exists_le with ⟨C', hC'⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
case intro.intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
have : ∀ x, C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C' := by simpa using hC'
case intro.intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ ‖f x‖ ≤ max C C' * ‖g'' x‖
case intro.intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
⊢ ∃ C, C > 0 ∧ ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
refine' ⟨max C C', lt_max_iff.2 (Or.inl C₀), fun x h₀ => _⟩
case intro.intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖
case intro.intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ ‖f x‖ ≤ max C C' * ‖g'' x‖
rw [max_mul_of_nonneg _ _ (norm_nonneg _), le_max_iff, or_iff_not_imp_left, not_le]
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖
exact fun hx => (div_le_iff (norm_pos_iff.2 h₀)).1 (this _ hx)
no goals
α : Type u_1
β : Type ?u.669259
E : Type u_2
F : Type ?u.669265
G : Type ?u.669268
E' : Type ?u.669271
F' : Type ?u.669274
G' : Type ?u.669277
E'' : Type ?u.669280
F'' : Type u_3
G'' : Type ?u.669286
R : Type ?u.669289
R' : Type ?u.669292
𝕜 : Type ?u.669295
𝕜' : Type ?u.669298
inst✝¹² : Norm E
inst✝¹¹ : Norm F
inst✝¹⁰ : Norm G
inst✝⁹ : SeminormedAddCommGroup E'
inst✝⁸ : SeminormedAddCommGroup F'
inst✝⁷ : SeminormedAddCommGroup G'
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedAddCommGroup F''
inst✝⁴ : NormedAddCommGroup G''
inst✝³ : SeminormedRing R
inst✝² : SeminormedRing R'
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
c c' c₁ c₂ : ℝ
f : α → E
g : α → F
k : α → G
f' : α → E'
g' : α → F'
k' : α → G'
f'' : α → E''
g'' : α → F''
k'' : α → G''
l l' : Filter α
h : f =O[cofinite] g''
C : ℝ
C₀ : 0 < C
hC : Set.Finite {x | ¬‖f x‖ ≤ C * ‖g'' x‖}
C' : ℝ
hC' : ∀ (i : ℝ), i ∈ Finset.image (fun x => ‖f x‖ / ‖g'' x‖) (Finite.toFinset hC) → i ≤ C'
⊢ ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
simpa using hC'