no goals
α : Type u_1
β : Type ?u.290943
E : Type u_2
F : Type u_3
G : Type ?u.290952
E' : Type ?u.290955
F' : Type ?u.290958
G' : Type ?u.290961
E'' : Type ?u.290964
F'' : Type ?u.290967
G'' : Type ?u.290970
R : Type ?u.290973
R' : Type ?u.290976
𝕜 : Type ?u.290979
𝕜' : Type ?u.290982
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 α
inst✝¹ : One F
inst✝ : NormOneClass F
c : E
l : Filter α
⊢ IsBigOWith ‖c‖ l (fun _x => c) fun _x => 1
simp [isBigOWith_iff]