awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
hs : Membership.mem (γ := Filter ℝ) atTop s
⊢ ∃ (a : ℝ), ∀ b ≥ a, b ∈ s

Tactic:
rw [mem_atTop_sets] at hs

Premises used: Filter.mem_atTop_sets
-- 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₃
hs : ∃ (a : ℝ), ∀ b ≥ a, b ∈ s
rcases : ∀ (l_1 : ℝ) (hl : ∀ b ≥ l_1, b ∈ s), Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
rcases hs with ⟨l, hl⟩
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : 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_1
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₃
l : ℝ
hl : ∀ b ≥ l, b ∈ s
⊢ Ioi l ⊆ s

Tactic:
have hl' : Ioi l ⊆ s := fun x hx => hl x (le_of_lt hx)
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : 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_1
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₃
l : ℝ
hl : ∀ b ≥ l, b ∈ s
hl' : Ioi l ⊆ s
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l_1

Tactic:
lhopital_zero_atTop_on_Ioi ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hftop hgtop hdiv

Premises used: And.right, HasDerivAt.lhopital_zero_atTop_on_Ioi
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : 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_1
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₃
l : ℝ
hl : ∀ b ≥ l, b ∈ s
hl' : Ioi l ⊆ s
refine_1 : ∀ x ∈ Ioi l, HasDerivAt f (f' x) x
refine_2 : ∀ x ∈ Ioi l, HasDerivAt g (g' x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l_1

Tactic:
refine lhopital_zero_atTop_on_Ioi ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hftop hgtop hdiv

Premises used: And.right, HasDerivAt.lhopital_zero_atTop_on_Ioi
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : 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_1
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₃
l : ℝ
hl : ∀ b ≥ l, b ∈ s
hl' : Ioi l ⊆ s
⊢ ∀ x ∈ Ioi l, HasDerivAt f (f' x) x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : 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_1
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₃
l : ℝ
hl : ∀ b ≥ l, b ∈ s
hl' : Ioi l ⊆ s
⊢ ∀ x ∈ Ioi l, HasDerivAt g (g' x) x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atBot, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
⊢ ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot 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 atBot, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atBot, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
⊢ ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot 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 atBot, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atBot, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
⊢ ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot 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 atBot, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atBot, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, g' y ≠ 0
⊢ Tendsto f atBot (𝓝 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 atBot, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atBot, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, g' y ≠ 0
hfbot₁ : Tendsto f atBot (𝓝 0)
⊢ Tendsto g atBot (𝓝 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 atBot, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atBot, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, g' y ≠ 0
hfbot₁ : Tendsto f atBot (𝓝 0)
hgbot₁ : Tendsto g atBot (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot 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 ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, g' y ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
rcases :
  ∀ (s₁ : Set ℝ) (hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁) (hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y),
    Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot 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 ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, g' y ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
rcases :
  ∀ (s₂ : Set ℝ) (hs₂ : Membership.mem (γ := Filter ℝ) atBot s₂) (hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y),
    Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot 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 ℝ) atBot v ∧ ∀ y ∈ v, g' y ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atBot s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
rcases :
  ∀ (s₃ : Set ℝ) (hs₃ : Membership.mem (γ := Filter ℝ) atBot s₃) (hg' : ∀ y ∈ s₃, g' y ≠ 0),
    Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l

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

Tactic:
have hs : s ∈ atBot := inter_mem (inter_mem hs₁ hs₂) hs₃
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atBot s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : Membership.mem (γ := Filter ℝ) atBot s₃
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : Membership.mem (γ := Filter ℝ) atBot s
⊢ ∃ (a : ℝ), ∀ b ≤ a, b ∈ s

Tactic:
rw [mem_atBot_sets] at hs

Premises used: Filter.mem_atBot_sets
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atBot s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : Membership.mem (γ := Filter ℝ) atBot s₃
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : ∃ (a : ℝ), ∀ b ≤ a, b ∈ s
rcases : ∀ (l_1 : ℝ) (hl : ∀ b ≤ l_1, b ∈ s), Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l

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

Tactic:
have hl' : Iio l ⊆ s := fun x hx => hl x (le_of_lt hx)
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l_1
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atBot s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : Membership.mem (γ := Filter ℝ) atBot s₃
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ b ≤ l, b ∈ s
hl' : Iio l ⊆ s
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l_1

Tactic:
lhopital_zero_atBot_on_Iio ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hfbot hgbot hdiv

Premises used: HasDerivAt.lhopital_zero_atBot_on_Iio, And.right
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l_1
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atBot s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : Membership.mem (γ := Filter ℝ) atBot s₃
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ b ≤ l, b ∈ s
hl' : Iio l ⊆ s
refine_1 : ∀ x ∈ Iio l, HasDerivAt f (f' x) x
refine_2 : ∀ x ∈ Iio l, HasDerivAt g (g' x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l_1

Tactic:
refine lhopital_zero_atBot_on_Iio ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hfbot hgbot hdiv

Premises used: HasDerivAt.lhopital_zero_atBot_on_Iio, And.right
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l_1
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atBot s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : Membership.mem (γ := Filter ℝ) atBot s₃
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ b ≤ l, b ∈ s
hl' : Iio l ⊆ s
⊢ ∀ x ∈ Iio l, HasDerivAt f (f' x) x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l_1 : Filter ℝ
f f' g g' : ℝ → ℝ
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l_1
s₁ : Set ℝ
hs₁ : Membership.mem (γ := Filter ℝ) atBot s₁
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : Membership.mem (γ := Filter ℝ) atBot s₂
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : Membership.mem (γ := Filter ℝ) atBot s₃
hg' : ∀ y ∈ s₃, g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ b ≤ l, b ∈ s
hl' : Iio l ⊆ s
⊢ ∀ x ∈ Iio l, HasDerivAt g (g' x) x

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ f (s \ {a}) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, derivWithin g (s \ {a}) x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x) (𝓝[s \ {a}] a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ g (s \ {a}) x

Tactic:
have hdg : ∀ᶠ x in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ g (s \ {a}) x :=
    hg'.mp (Eventually.of_forall fun _ hg' =>
      by_contradiction fun h => hg' (derivWithin_zero_of_not_differentiableWithinAt h))
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ f (s \ {a}) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, derivWithin g (s \ {a}) x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x) (𝓝[s \ {a}] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ g (s \ {a}) x
⊢ ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt f (derivWithin f (s \ {a}) x) (s \ {a}) x

Tactic:
have hdf' : ∀ᶠ x in 𝓝[s \ {a}] a, HasDerivWithinAt f (derivWithin f (s \ {a}) x) (s \ {a}) x :=
    hdf.mp (Eventually.of_forall fun _ h ↦ h.hasDerivWithinAt)
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ f (s \ {a}) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, derivWithin g (s \ {a}) x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x) (𝓝[s \ {a}] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ g (s \ {a}) x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt f (derivWithin f (s \ {a}) x) (s \ {a}) x
⊢ ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt g (derivWithin g (s \ {a}) x) (s \ {a}) x

Tactic:
have hdg' : ∀ᶠ x in 𝓝[s \ {a}] a, HasDerivWithinAt g (derivWithin g (s \ {a}) x) (s \ {a}) x :=
    hdg.mp (Eventually.of_forall fun _ h => h.hasDerivWithinAt)
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ f (s \ {a}) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, derivWithin g (s \ {a}) x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x) (𝓝[s \ {a}] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ g (s \ {a}) x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt f (derivWithin f (s \ {a}) x) (s \ {a}) x
hdg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt g (derivWithin g (s \ {a}) x) (s \ {a}) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
HasDerivWithinAt.lhopital_zero_nhdsWithin_convex hs hdf' hdg' hg' hfa hga hdiv

Premises used: HasDerivWithinAt.lhopital_zero_nhdsWithin_convex
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ f (s \ {a}) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, derivWithin g (s \ {a}) x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x) (𝓝[s \ {a}] a) l
hdg : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableWithinAt ℝ g (s \ {a}) x
hdf' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt f (derivWithin f (s \ {a}) x) (s \ {a}) x
hdg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivWithinAt g (derivWithin g (s \ {a}) x) (s \ {a}) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
exact HasDerivWithinAt.lhopital_zero_nhdsWithin_convex hs hdf' hdg' hg' hfa hga hdiv

Premises used: HasDerivWithinAt.lhopital_zero_nhdsWithin_convex
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
derivWithin.lhopital_zero_nhdsWithin_convex hs
    (hdf.mono fun _ h ↦ h.differentiableWithinAt) (hg'.mp ?_) hfa hga
    (hdiv.congr' ?_)

Premises used: DifferentiableAt.differentiableWithinAt, Filter.Eventually.mono, Filter.Eventually.mp, Filter.Tendsto.congr', derivWithin.lhopital_zero_nhdsWithin_convex
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
refine_1 : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0 → derivWithin g (s \ {a}) x ≠ 0
refine_2 :
  (𝓝[s \ {a}] a).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ deriv f x / deriv g x) fun (x : ℝ) ↦
    derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l

Tactic:
refine derivWithin.lhopital_zero_nhdsWithin_convex hs
    (hdf.mono fun _ h ↦ h.differentiableWithinAt) (hg'.mp ?_) hfa hga
    (hdiv.congr' ?_)

Premises used: DifferentiableAt.differentiableWithinAt, Filter.Eventually.mono, Filter.Eventually.mp, Filter.Tendsto.congr', derivWithin.lhopital_zero_nhdsWithin_convex
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
refine_1 : ∀ (x : ℝ), s \ {a} ∈ 𝓝 x → deriv g x ≠ 0 → derivWithin g (s \ {a}) x ≠ 0
⊢ ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0 → derivWithin g (s \ {a}) x ≠ 0

Tactic:
apply (hs.diff_singleton_eventually_mem_nhds a).mono

Premises used: Filter.Eventually.mono, Convex.diff_singleton_eventually_mem_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
refine_2 :
  ∀ (x : ℝ),
    s \ {a} ∈ 𝓝 x →
      Eq (α := ℝ) ((fun (x : ℝ) ↦ deriv f x / deriv g x) x)
        ((fun (x : ℝ) ↦ derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x) x)
⊢ (𝓝[s \ {a}] a).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ deriv f x / deriv g x) fun (x : ℝ) ↦
    derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x

Tactic:
apply (hs.diff_singleton_eventually_mem_nhds a).mono

Premises used: Filter.Eventually.mono, Convex.diff_singleton_eventually_mem_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
x : ℝ
h : s \ {a} ∈ 𝓝 x
h_1 : deriv g x ≠ 0
refine_1 refine_1₁ refine_1₂ refine_1₃ : deriv g x ≠ 0
⊢ derivWithin g (s \ {a}) x ≠ 0

Tactic:
rwa [derivWithin_of_mem_nhds ‹_›]

Premises used: derivWithin_of_mem_nhds