-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_nhds_left (hdf : ∀ᶠ x in 𝓝[<] a, DifferentiableAt ℝ f x)
    (hg' : ∀ᶠ x in 𝓝[<] a, deriv g x ≠ 0) (hfa : Tendsto f (𝓝[<] a) (𝓝 0))
    (hga : Tendsto g (𝓝[<] a) (𝓝 0))
    (hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) (𝓝[<] a) l) :
    Tendsto (fun x => f x / g x) (𝓝[<] a) l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (deriv f x) x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l

Tactic:
have hdg' : ∀ᶠ x in 𝓝[<] a, HasDerivAt g (deriv g x) x :=
  hdg.mp (Eventually.of_forall fun _ => DifferentiableAt.hasDerivAt)

Result:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l

Tactic:
have hdf' : ∀ᶠ x in 𝓝[<] a, HasDerivAt f (deriv f x) x :=
  hdf.mp (Eventually.of_forall fun _ => DifferentiableAt.hasDerivAt)

Result:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (deriv f x) x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l

Tactic:
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))

Result:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l

Tactic:
exact HasDerivAt.lhopital_zero_nhds_left hdf' hdg' hg' hfa hga hdiv

Result:
no goals