a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio b] b) l
hdf : ∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
have hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x := fun x hx =>
  (hdf x hx).differentiableAt (Ioo_mem_nhds hx.1 hx.2)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio b] b) l
hdf : ∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
hdg : ∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio b] b) l
hdf : ∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
have hdg : ∀ x ∈ Ioo a b, 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 (Ioo a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio b] b) l
hdf : ∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ f x
hdg : ∀ (x : ℝ), x ∈ Ioo a b → DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
exact HasDerivAt.lhopital_zero_left_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
  (fun x hx => (hdg x hx).hasDerivAt) hg' hfb hgb hdiv