awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : s ∩ Iio a = ∅
hs_Ioi : s ∩ Ioi a = ∅
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
simp [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left, hs_Iio, hs_Ioi]

Premises used: Set.diff_eq, Set.Iio_union_Ioi, Set.inter_union_distrib_left
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : s ∩ Iio a = ∅
hs_Ioi : (s ∩ Ioi a).Nonempty
inl :
  ∀ (hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0) (hfa : Tendsto f (𝓝[>] a) (𝓝 0)) (hga : Tendsto g (𝓝[>] a) (𝓝 0))
    (hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l) (h : ∀ᶠ (x : ℝ) in 𝓝[>] a, s \ {a} ∈ 𝓝 x)
    (hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x) (hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
simp_rw [hs.nhdsWithin_diff_eq_nhdsGT has hs_Iio hs_Ioi] at *

Premises used: Convex.nhdsWithin_diff_eq_nhdsGT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
has : a ∈ closure s
hs_Iio : s ∩ Iio a = ∅
hs_Ioi : (s ∩ Ioi a).Nonempty
hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
lhopital_zero_nhdsGT hff' hgg' hg' hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_nhdsGT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
has : a ∈ closure s
hs_Iio : s ∩ Iio a = ∅
hs_Ioi : (s ∩ Ioi a).Nonempty
hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
h : ∀ᶠ (x : ℝ) in 𝓝[>] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
exact lhopital_zero_nhdsGT hff' hgg' hg' hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_nhdsGT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : s ∩ Ioi a = ∅
inr :
  ∀ (hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0) (hfa : Tendsto f (𝓝[<] a) (𝓝 0)) (hga : Tendsto g (𝓝[<] a) (𝓝 0))
    (hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l) (h : ∀ᶠ (x : ℝ) in 𝓝[<] a, s \ {a} ∈ 𝓝 x)
    (hff' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x) (hgg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
simp_rw [hs.nhdsWithin_diff_eq_nhdsLT has hs_Iio hs_Ioi] at *

Premises used: Convex.nhdsWithin_diff_eq_nhdsLT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
has : a ∈ closure s
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : s ∩ Ioi a = ∅
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l

Tactic:
lhopital_zero_nhdsLT hff' hgg' hg' hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_nhdsLT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
has : a ∈ closure s
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : s ∩ Ioi a = ∅
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l

Tactic:
exact lhopital_zero_nhdsLT hff' hgg' hg' hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_nhdsLT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, g' x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[s \ {a}] a) l
has : a ∈ closure s
h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : (s ∩ Ioi a).Nonempty
inr :
  ∀ (hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0) (hfa : Tendsto f (𝓝[≠] a) (𝓝 0)) (hga : Tendsto g (𝓝[≠] a) (𝓝 0))
    (hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[≠] a) l) (h : ∀ᶠ (x : ℝ) in 𝓝[≠] a, s \ {a} ∈ 𝓝 x)
    (hff' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x) (hgg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
simp_rw [hs.nhdsWithin_diff_eq_nhdsNE has hs_Iio hs_Ioi] at *

Premises used: Convex.nhdsWithin_diff_eq_nhdsNE
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
has : a ∈ closure s
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : (s ∩ Ioi a).Nonempty
hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0
hfa : Tendsto f (𝓝[≠] a) (𝓝 0)
hga : Tendsto g (𝓝[≠] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[≠] a) l
h : ∀ᶠ (x : ℝ) in 𝓝[≠] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l

Tactic:
lhopital_zero_nhdsNE hff' hgg' hg' hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_nhdsNE
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
has : a ∈ closure s
hs_Iio : (s ∩ Iio a).Nonempty
hs_Ioi : (s ∩ Ioi a).Nonempty
hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0
hfa : Tendsto f (𝓝[≠] a) (𝓝 0)
hga : Tendsto g (𝓝[≠] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[≠] a) l
h : ∀ᶠ (x : ℝ) in 𝓝[≠] a, s \ {a} ∈ 𝓝 x
hff' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l

Tactic:
exact lhopital_zero_nhdsNE hff' hgg' hg' hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_nhdsNE
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hff'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x
hgg'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x
hg'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0
hfa₁ : Tendsto f (𝓝[≠] a) (𝓝 0)
hga₁ : Tendsto g (𝓝[≠] a) (𝓝 0)
hdiv₁ : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[≠] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l

Tactic:
apply @lhopital_zero_nhdsNE _ _ _ f' _ g'

Premises used: HasDerivAt.lhopital_zero_nhdsNE
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hff'₁ : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x

Tactic:
apply eventually_nhdsWithin_of_eventually_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hff'₁ : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hgg'₁ : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x

Tactic:
apply eventually_nhdsWithin_of_eventually_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hgg'₁ : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hg'₁ : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0

Tactic:
apply eventually_nhdsWithin_of_eventually_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hg'₁ : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hfa₁ : Tendsto f (𝓝 a) (𝓝 0)
⊢ Tendsto f (𝓝[≠] a) (𝓝 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hfa₁ : Tendsto f (𝓝 a) (𝓝 0)
⊢ Tendsto f (𝓝[≠] a) (𝓝 0)

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hga₁ : Tendsto g (𝓝 a) (𝓝 0)
⊢ Tendsto g (𝓝[≠] a) (𝓝 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
hga₁ : Tendsto g (𝓝 a) (𝓝 0)
⊢ Tendsto g (𝓝[≠] a) (𝓝 0)

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv hdiv₁ : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
⊢ Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[≠] a) l

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv hdiv₁ : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
⊢ Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[≠] a) l

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
⊢ Tendsto f (𝓝 a) (𝓝 0)

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
⊢ Tendsto g (𝓝 a) (𝓝 0)

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝 a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, g' x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l
⊢ Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝 a) l

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
⊢ ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
⊢ ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
⊢ ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, g' y ≠ 0

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, g' y ≠ 0
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, g' y ≠ 0
hftop₁ : Tendsto f atTop (𝓝 0)
⊢ Tendsto g atTop (𝓝 0)

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, g' y ≠ 0
hftop₁ : Tendsto f atTop (𝓝 0)
hgtop₁ : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
rcases :
  ∀ (s₁ : Set ℝ) (hs₁ : Membership.mem (γ := Filter ℝ) atTop s₁) (hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y),
    Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
rcases hff' with ⟨s₁, hs₁, hff'⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atTop s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
rcases :
  ∀ (s₂ : Set ℝ) (hs₂ : Membership.mem (γ := Filter ℝ) atTop s₂) (hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y),
    Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
rcases hgg' with ⟨s₂, hs₂, hgg'⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hg' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atTop s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atTop s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
rcases :
  ∀ (s₃ : Set ℝ) (hs₃ : Membership.mem (γ := Filter ℝ) atTop s₃) (hg' : ∀ y ∈ s₃, g' y ≠ 0),
    Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
rcases hg' with ⟨s₃, hs₃, hg'⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atTop s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atTop s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : Membership.mem (γ := Filter ℝ) atTop s₃
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
⊢ Membership.mem (γ := Filter ℝ) atTop s

Tactic:
have hs : s ∈ atTop := inter_mem (inter_mem hs₁ hs₂) hs₃