theorem Filter.Tendsto.of_div {X : Set ℝ} {f g : ℝ → ℝ} {x₀ f'x₀ g'x₀ : ℝ} (hfx₀ : f x₀ = 0) (hgx₀ : g x₀ = 0) (hg_non : g'x₀ ≠ 0) (hf'x₀ : HasDerivWithinAt f f'x₀ X x₀) (hg'x₀ : HasDerivWithinAt g g'x₀ X x₀) : (∃ δ > 0, ∀ x ∈ X \ {x₀} ∩ Set.Ioo (x₀ - δ) (x₀ + δ), g x ≠ 0) ∧ Tendsto (fun (x : ℝ) => f x / g x) (nhdsWithin x₀ (X \ {x₀})) (nhds (f'x₀ / g'x₀))

Proposition 10.5.1 (L'Hôpital's rule, I) / Exercise 10.5.1

theorem Filter.Tendsto.of_div' {a b L : ℝ} (hab : a < b) {f g f' g' : ℝ → ℝ} (hf : DifferentiableOn ℝ f (Set.Icc a b)) (hg : DifferentiableOn ℝ g (Set.Icc a b)) (hf' : f' = derivWithin f (Set.Icc a b)) (hg' : g' = derivWithin g (Set.Icc a b)) (hfa : f a = 0) (hga : g a = 0) (hgnon : ∀ x ∈ Set.Icc a b, g' x ≠ 0) (hderiv : Tendsto (fun (x : ℝ) => f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)) : (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Tendsto (fun (x : ℝ) => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)

Proposition 10.5.2 (L'Hôpital's rule, II)