no goals
α : Type u_2
β : Type ?u.44090
E : Type u_3
F : Type ?u.44096
G : Type ?u.44099
E' : Type ?u.44102
F' : Type u_4
G' : Type ?u.44108
E'' : Type ?u.44111
F'' : Type ?u.44114
G'' : Type ?u.44117
R : Type ?u.44120
R' : Type ?u.44123
𝕜 : Type ?u.44126
𝕜' : Type ?u.44129
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 α
ι : Sort u_1
p : ι → Prop
s : ι → Set α
h✝ : f =O[l] g'
hb : HasBasis l p s
c : ℝ
_hc : 0 < c
h : IsBigOWith c l f g'
⊢ ∃ i _hi, ∀ (x : α), x ∈ s i → ‖f x‖ ≤ c * ‖g' x‖
simpa only [isBigOWith_iff, hb.eventually_iff, exists_prop] using h