a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio a] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio a] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l
have hdg : ∀ᶠ x in 𝓝[<] a, DifferentiableAt ℝ g x :=
  hg'.mp (eventually_of_forall fun _ hg' =>
    by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h))
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio a] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt f (deriv f x) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio a] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l
have hdf' : ∀ᶠ x in 𝓝[<] a, HasDerivAt f (deriv f x) x :=
  hdf.mp (eventually_of_forall fun _ => DifferentiableAt.hasDerivAt)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio a] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio a] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt f (deriv f x) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l
have hdg' : ∀ᶠ x in 𝓝[<] a, HasDerivAt g (deriv g x) x :=
  hdg.mp (eventually_of_forall fun _ => DifferentiableAt.hasDerivAt)
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Iio a] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l
exact HasDerivAt.lhopital_zero_nhds_left hdf' hdg' hg' hfa hga hdiv