no goals
α : Type u_1
x y z : ℝ
l : Filter α
f g : α → ℝ
⊢ ((fun x => exp (f x)) =o[l] fun x => exp (g x)) ↔ Tendsto (fun x => g x - f x) l atTop
simp only [isLittleO_iff_tendsto, exp_ne_zero, ← exp_sub, ← tendsto_neg_atTop_iff, false_imp_iff,
  imp_true_iff, tendsto_exp_comp_nhds_zero, neg_sub]