awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
rcases :
  ∀ (s₁ : Set ℝ) (hs₁ : s₁ ∈ 𝓝[>] a) (hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
rcases hff' with ⟨s₁, hs₁, hff'⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
rcases :
  ∀ (s₂ : Set ℝ) (hs₂ : s₂ ∈ 𝓝[>] a) (hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
rcases hgg' with ⟨s₂, hs₂, hgg'⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
rcases : ∀ (s₃ : Set ℝ) (hs₃ : s₃ ∈ 𝓝[>] a) (hg' : ∀ y ∈ s₃, g' y ≠ 0), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

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

Tactic:
have hs : s ∈ 𝓝[>] a := inter_mem (inter_mem hs₁ hs₂) hs₃
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[>] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : s ∈ 𝓝[>] a
⊢ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
rw [mem_nhdsGT_iff_exists_Ioo_subset] at hs

Premises used: mem_nhdsGT_iff_exists_Ioo_subset
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[>] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : ∃ u ∈ Ioi a, Ioo a u ⊆ s
rcases : ∀ (u : ℝ) (hau : u ∈ Ioi a) (hu : Ioo a u ⊆ s), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
rcases hs with ⟨u, hau, hu⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[>] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
u : ℝ
hau : u ∈ Ioi a
hu : Ioo a u ⊆ s
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
lhopital_zero_right_on_Ioo hau ?_ ?_ ?_ hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_right_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[>] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
u : ℝ
hau : u ∈ Ioi a
hu : Ioo a u ⊆ s
refine_1 : ∀ x ∈ Ioo a u, HasDerivAt f (f' x) x
refine_2 : ∀ x ∈ Ioo a u, HasDerivAt g (g' x) x
refine_3 : ∀ x ∈ Ioo a u, g' x ≠ 0
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
refine lhopital_zero_right_on_Ioo hau ?_ ?_ ?_ hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_right_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[>] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
u : ℝ
hau : u ∈ Ioi a
hu : Ioo a u ⊆ s
⊢ ∀ x ∈ Ioo a u, HasDerivAt f (f' x) x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[>] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
u : ℝ
hau : u ∈ Ioi a
hu : Ioo a u ⊆ s
⊢ ∀ x ∈ Ioo a u, HasDerivAt g (g' x) x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[>] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
u : ℝ
hau : u ∈ Ioi a
hu : Ioo a u ⊆ s
⊢ ∀ x ∈ Ioo a u, g' x ≠ 0

Tactic:
grind
-- 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
⊢ ∃ v ∈ 𝓝[<] a, ∀ 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:
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'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y
⊢ ∃ v ∈ 𝓝[<] a, ∀ 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:
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'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
⊢ ∃ v ∈ 𝓝[<] a, ∀ 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:
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'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
⊢ Tendsto f (𝓝[<] a) (𝓝 0)

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- 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'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
hfa₁ : Tendsto f (𝓝[<] a) (𝓝 0)
⊢ Tendsto g (𝓝[<] a) (𝓝 0)

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- 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'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
hfa₁ : Tendsto f (𝓝[<] a) (𝓝 0)
hga₁ : Tendsto g (𝓝[<] a) (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l
rcases :
  ∀ (s₁ : Set ℝ) (hs₁ : s₁ ∈ 𝓝[<] a) (hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l

Tactic:
rcases hff' with ⟨s₁, hs₁, hff'⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
rcases :
  ∀ (s₂ : Set ℝ) (hs₂ : s₂ ∈ 𝓝[<] a) (hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l

Tactic:
rcases hgg' with ⟨s₂, hs₂, hgg'⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hg' : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
rcases : ∀ (s₃ : Set ℝ) (hs₃ : s₃ ∈ 𝓝[<] a) (hg' : ∀ y ∈ s₃, g' y ≠ 0), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l

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

Tactic:
have hs : s ∈ 𝓝[<] a := inter_mem (inter_mem hs₁ hs₂) hs₃
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[<] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : s ∈ 𝓝[<] a
⊢ ∃ l ∈ Iio a, Ioo l a ⊆ s

Tactic:
rw [mem_nhdsLT_iff_exists_Ioo_subset] at hs

Premises used: mem_nhdsLT_iff_exists_Ioo_subset
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[<] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : ∃ l ∈ Iio a, Ioo l a ⊆ s
rcases : ∀ (l_1 : ℝ) (hal : l_1 ∈ Iio a) (hl : Ioo l_1 a ⊆ s), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l

Tactic:
rcases hs with ⟨l, hal, hl⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l_1
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[<] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hal : l ∈ Iio a
hl : Ioo l a ⊆ s
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l_1

Tactic:
lhopital_zero_left_on_Ioo hal ?_ ?_ ?_ hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_left_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l_1
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[<] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hal : l ∈ Iio a
hl : Ioo l a ⊆ s
refine_1 : ∀ x ∈ Ioo l a, HasDerivAt f (f' x) x
refine_2 : ∀ x ∈ Ioo l a, HasDerivAt g (g' x) x
refine_3 : ∀ x ∈ Ioo l a, g' x ≠ 0
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l_1

Tactic:
refine lhopital_zero_left_on_Ioo hal ?_ ?_ ?_ hfa hga hdiv

Premises used: HasDerivAt.lhopital_zero_left_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l_1
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[<] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hal : l ∈ Iio a
hl : Ioo l a ⊆ s
⊢ ∀ x ∈ Ioo l a, HasDerivAt f (f' x) x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l_1
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[<] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hal : l ∈ Iio a
hl : Ioo l a ⊆ s
⊢ ∀ x ∈ Ioo l a, HasDerivAt g (g' x) x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l_1
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[<] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[<] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ 𝓝[<] a
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hal : l ∈ Iio a
hl : Ioo l a ⊆ s
⊢ ∀ x ∈ Ioo l a, g' x ≠ 0

Tactic:
grind
-- 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
simp :
  ∀ (hff' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x)
    (hgg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x)
    (hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0)
    (hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0))
    (hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0))
    (hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l ∧ Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l ∧ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l

Tactic:
simp only [← Iio_union_Ioi, nhdsWithin_union, tendsto_sup, eventually_sup] at *

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

Tactic:
⟨lhopital_zero_nhdsLT hff'.1 hgg'.1 hg'.1 hfa.1 hga.1 hdiv.1,
    lhopital_zero_nhdsGT hff'.2 hgg'.2 hg'.2 hfa.2 hga.2 hdiv.2⟩

Premises used: HasDerivAt.lhopital_zero_nhdsGT, And.right, And.left, And.intro, HasDerivAt.lhopital_zero_nhdsLT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt f (f' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, HasDerivAt g (g' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, g' x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] a) l ∧ Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l ∧ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
exact ⟨lhopital_zero_nhdsLT hff'.1 hgg'.1 hg'.1 hfa.1 hga.1 hdiv.1,
    lhopital_zero_nhdsGT hff'.2 hgg'.2 hg'.2 hfa.2 hga.2 hdiv.2⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt f (f' x) (s \ {a}) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt g (g' x) (s \ {a}) x
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 : (𝓝[s \ {a}] a).NeBot
⊢ a ∈ closure s

Tactic:
replace has := closure_mono diff_subset (mem_closure_iff_nhdsWithin_neBot.2 has)
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt f (f' x) (s \ {a}) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt g (g' x) (s \ {a}) x
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
⊢ ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x

Tactic:
have h := hs.diff_singleton_eventually_mem_nhds a
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hff' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt f (f' x) (s \ {a}) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt g (g' x) (s \ {a}) x
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
⊢ ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x

Tactic:
replace hff' := h.mp <| hff'.mono fun _ h ↦ h.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hgg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt g (g' x) (s \ {a}) x
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
⊢ ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x

Tactic:
replace hgg' := h.mp <| hgg'.mono fun _ h ↦ h.hasDerivAt
-- 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
inl : ∀ (hs_Iio : s ∩ Iio a = ∅), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
inr : ∀ (hs_Iio : (s ∩ Iio a).Nonempty), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
rcases eq_empty_or_nonempty (s ∩ Iio a) with hs_Iio | hs_Iio

Premises used: Inter.inter, Set.eq_empty_or_nonempty, Set.Iio
-- 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 = ∅
inl : ∀ (hs_Ioi : s ∩ Ioi a = ∅), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
inl₁ : ∀ (hs_Ioi : (s ∩ Ioi a).Nonempty), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
rcases eq_empty_or_nonempty (s ∩ Ioi a) with hs_Ioi | hs_Ioi

Premises used: Set.Ioi, Inter.inter, Set.eq_empty_or_nonempty
-- 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
inr : ∀ (hs_Ioi : s ∩ Ioi a = ∅), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
inr₁ : ∀ (hs_Ioi : (s ∩ Ioi a).Nonempty), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
rcases eq_empty_or_nonempty (s ∩ Ioi a) with hs_Ioi | hs_Ioi

Premises used: Set.Ioi, Inter.inter, Set.eq_empty_or_nonempty