no goals
α : Type u_1
β : Type ?u.294672
E : Type ?u.294675
F : Type u_3
G : Type ?u.294681
E' : Type u_2
F' : Type ?u.294687
G' : Type ?u.294690
E'' : Type ?u.294693
F'' : Type ?u.294696
G'' : Type ?u.294699
R : Type ?u.294702
R' : Type ?u.294705
𝕜 : Type ?u.294708
𝕜' : Type ?u.294711
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
⊢ (f' =o[l] fun _x => 1) ↔ Tendsto f' l (𝓝 0)
simp only [isLittleO_iff, norm_one, mul_one, Metric.nhds_basis_closedBall.tendsto_right_iff,
  Metric.mem_closedBall, dist_zero_right]