∀ {a b : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  a < b →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x) →
        (∀ x ∈ Set.Ioo a b, g' x ≠ 0) →
          Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds 0) →
            Filter.Tendsto g (nhdsWithin b (Set.Iio b)) (nhds 0) →
              Filter.Tendsto (fun x => f' x / g' x) (nhdsWithin b (Set.Iio b)) l →
                Filter.Tendsto (fun x => f x / g x) (nhdsWithin b (Set.Iio b)) l