a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Iio a)
hg' : ∀ (x : ℝ), x ∈ Iio a → deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
hdf : ∀ (x : ℝ), x ∈ Iio a → DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) atBot l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Iio a)
hg' : ∀ (x : ℝ), x ∈ Iio a → deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
⊢ Tendsto (fun x => f x / g x) atBot l
have hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x := fun x hx =>
  (hdf x hx).differentiableAt (Iio_mem_nhds hx)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Iio a)
hg' : ∀ (x : ℝ), x ∈ Iio a → deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
hdf : ∀ (x : ℝ), x ∈ Iio a → DifferentiableAt ℝ f x
hdg : ∀ (x : ℝ), x ∈ Iio a → DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) atBot l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Iio a)
hg' : ∀ (x : ℝ), x ∈ Iio a → deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
hdf : ∀ (x : ℝ), x ∈ Iio a → DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) atBot l
have hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x := fun x hx =>
  by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Iio a)
hg' : ∀ (x : ℝ), x ∈ Iio a → deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
hdf : ∀ (x : ℝ), x ∈ Iio a → DifferentiableAt ℝ f x
hdg : ∀ (x : ℝ), x ∈ Iio a → DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) atBot l
exact HasDerivAt.lhopital_zero_atBot_on_Iio (fun x hx => (hdf x hx).hasDerivAt)
  (fun x hx => (hdg x hx).hasDerivAt) hg' hfbot hgbot hdiv