awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
Tactic: rw [eventually_iff_exists_mem] at *
Cleared hypotheses: hff', hgg', hg', hfbot, hgbot, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
Tactic: rw [eventually_iff_exists_mem] at *
Cleared hypotheses: hff', hgg', hg', hfbot, hgbot, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atBot v ∧ ∀ y ∈ v, g' y ≠ 0
Tactic: rw [eventually_iff_exists_mem] at *
Cleared hypotheses: hff', hgg', hg', hfbot, hgbot, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have 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
Tactic: rcases hff' with ⟨s₁, hs₁, hff'⟩
Cleared hypotheses: hff'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have 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
Tactic: rcases hgg' with ⟨s₂, hs₂, hgg'⟩
Cleared hypotheses: hgg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have rcases : ∀ (s₃ : Set ℝ) (hs₃ : Membership.mem (γ := Filter ℝ) atBot s₃) (hg' : ∀ y ∈ s₃, g' y ≠ 0),
  Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
Tactic: rcases hg' with ⟨s₃, hs₃, hg'⟩
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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₃
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hs : Membership.mem (γ := Filter ℝ) atBot s
Tactic: have hs : s ∈ atBot := inter_mem (inter_mem hs₁ hs₂) hs₃
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hs₄ : ∃ (a : ℝ), ∀ b ≤ a, b ∈ s
Tactic: rw [mem_atBot_sets] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have rcases : ∀ (l_1 : ℝ) (hl : ∀ b ≤ l_1, b ∈ s), Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
Tactic: rcases hs with ⟨l, hl⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l_1
have hl' : Iio l ⊆ s
Tactic: have hl' : Iio l ⊆ s := fun x hx => hl x (le_of_lt hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
have refine_1 : ∀ x ∈ Iio l, HasDerivAt f (f' x) x
Tactic: refine lhopital_zero_atBot_on_Iio ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hfbot hgbot hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l_1
have refine_2 : ∀ x ∈ Iio l, HasDerivAt g (g' x) x
Tactic: refine lhopital_zero_atBot_on_Iio ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hfbot hgbot hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have hdg : ∀ᶠ (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))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have hdf' : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have hdg' : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
have refine_1 : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0 → derivWithin g (s \ {a}) x ≠ 0
Tactic: refine derivWithin.lhopital_zero_nhdsWithin_convex hs
    (hdf.mono fun _ h ↦ h.differentiableWithinAt) (hg'.mp ?_) hfa hga
    (hdiv.congr' ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have 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
Tactic: refine derivWithin.lhopital_zero_nhdsWithin_convex hs
    (hdf.mono fun _ h ↦ h.differentiableWithinAt) (hg'.mp ?_) hfa hga
    (hdiv.congr' ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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 : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0 → derivWithin g (s \ {a}) x ≠ 0
have refine_1 : ∀ (x : ℝ), s \ {a} ∈ 𝓝 x → deriv g x ≠ 0 → derivWithin g (s \ {a}) x ≠ 0
Tactic: apply (hs.diff_singleton_eventually_mem_nhds a).mono
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ (𝓝[s \ {a}] a).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ deriv f x / deriv g x) fun (x : ℝ) ↦
    derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x
have 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)
Tactic: apply (hs.diff_singleton_eventually_mem_nhds a).mono
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ deriv f x / deriv g x = derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x
have refine_2 : deriv f x / deriv g x = deriv f x / derivWithin g (s \ {a}) x
Tactic: rw [derivWithin_of_mem_nhds ‹_›]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ deriv f x / deriv g x = deriv f x / derivWithin g (s \ {a}) x
have refine_2 : deriv f x / deriv g x = deriv f x / deriv g x
Tactic: rw [derivWithin_of_mem_nhds ‹_›]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ deriv f x / deriv g x = derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x
have refine_2 : deriv f x / deriv g x = deriv f x / derivWithin g (s \ {a}) x
Tactic: iterate 2 rw [derivWithin_of_mem_nhds ‹_›]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
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
have rw : ∀ (hdf : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, deriv g x ≠ 0)
  (hfa : Tendsto f (𝓝[Ici a \ {a}] a) (𝓝 0)) (hga : Tendsto g (𝓝[Ici a \ {a}] a) (𝓝 0))
  (hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[Ici a \ {a}] a) l),
  Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Ici a \ {a}] a) l
Tactic: rw [← Ici_diff_left] at *
Cleared hypotheses: hdf, hg', hfa, hga, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
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
have rw : ∀ (hdf : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, deriv g x ≠ 0)
  (hfa : Tendsto f (𝓝[Iic a \ {a}] a) (𝓝 0)) (hga : Tendsto g (𝓝[Iic a \ {a}] a) (𝓝 0))
  (hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[Iic a \ {a}] a) l),
  Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Iic a \ {a}] a) l
Tactic: rw [← Iic_diff_right] at *
Cleared hypotheses: hdf, hg', hfa, hga, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
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
have rw : ∀ (hdf : ∀ᶠ (x : ℝ) in 𝓝[univ \ {a}] a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ (x : ℝ) in 𝓝[univ \ {a}] a, deriv g x ≠ 0)
  (hfa : Tendsto f (𝓝[univ \ {a}] a) (𝓝 0)) (hga : Tendsto g (𝓝[univ \ {a}] a) (𝓝 0))
  (hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[univ \ {a}] a) l),
  Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[univ \ {a}] a) l
Tactic: rw [compl_eq_univ_diff] at *
Cleared hypotheses: hdf, hg', hfa, hga, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
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
have hdf₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x
Tactic: apply lhopital_zero_nhdsNE
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
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
hdf₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hg'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0
Tactic: apply lhopital_zero_nhdsNE
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
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
hdf₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x
hg'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hfa₁ : Tendsto f (𝓝[≠] a) (𝓝 0)
Tactic: apply lhopital_zero_nhdsNE
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
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
hdf₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x
hg'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0
hfa₁ : Tendsto f (𝓝[≠] a) (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hga₁ : Tendsto g (𝓝[≠] a) (𝓝 0)
Tactic: apply lhopital_zero_nhdsNE
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
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
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)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hdiv₁ : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[≠] a) l
Tactic: apply lhopital_zero_nhdsNE
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
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
have hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
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))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
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
have hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x
Tactic: have hdf' : ∀ᶠ x in atTop, HasDerivAt f (deriv f x) x :=
    hdf.mono fun _ => DifferentiableAt.hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
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
have hdg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (deriv g x) x
Tactic: have hdg' : ∀ᶠ x in atTop, HasDerivAt g (deriv g x) x :=
    hdg.mono fun _ => DifferentiableAt.hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atBot l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x
Tactic: have hdg : ∀ᶠ x in atBot, DifferentiableAt ℝ g x :=
    hg'.mono fun _ hg' => by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atBot l
hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hdf' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x
Tactic: have hdf' : ∀ᶠ x in atBot, HasDerivAt f (deriv f x) x :=
    hdf.mono fun _ => DifferentiableAt.hasDerivAt