∀ {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in Filter.atBot, HasDerivAt f (f' x) x) →
    (∀ᶠ (x : ℝ) in Filter.atBot, HasDerivAt g (g' x) x) →
      (∀ᶠ (x : ℝ) in Filter.atBot, g' x ≠ 0) →
        Filter.Tendsto f Filter.atBot (nhds 0) →
          Filter.Tendsto g Filter.atBot (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) Filter.atBot l → Filter.Tendsto (fun x => f x / g x) Filter.atBot l