-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_atTop (hdf : ∀ᶠ x : ℝ in atTop, DifferentiableAt ℝ f x)
    (hg' : ∀ᶠ x : ℝ in atTop, deriv g x ≠ 0) (hftop : Tendsto f atTop (𝓝 0))
    (hgtop : Tendsto g atTop (𝓝 0)) (hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) atTop l) :
    Tendsto (fun x => f x / g x) atTop l

Proof state:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x
⊢ Tendsto (fun x => f x / g x) atTop l

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

Result:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun x => f x / g x) atTop l

Proof state:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun x => f x / g x) atTop l

Tactic:
exact HasDerivAt.lhopital_zero_atTop hdf' hdg' hg' hftop hgtop hdiv

Result:
no goals

Proof state:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
⊢ Tendsto (fun x => f x / g x) atTop l

Tactic:
have hdg : ∀ᶠ x in atTop, DifferentiableAt ℝ g x := hg'.mp
  (Eventually.of_forall fun _ hg' =>
    by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h))

Result:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) atTop l

Proof state:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) atTop l

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

Result:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x
⊢ Tendsto (fun x => f x / g x) atTop l