awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
have 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
Tactic: simp only [← Iio_union_Ioi, nhdsWithin_union, tendsto_sup, eventually_sup] at *
Cleared hypotheses: hff', hgg', hg', hfa, hga, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have has₁ : a ∈ closure s
Tactic: replace has := closure_mono diff_subset (mem_closure_iff_nhdsWithin_neBot.2 has)
Cleared hypotheses: has
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have h : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, s \ {a} ∈ 𝓝 x
Tactic: have h := hs.diff_singleton_eventually_mem_nhds a
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have hff'₁ : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt f (f' x) x
Tactic: replace hff' := h.mp <| hff'.mono fun _ h ↦ h.hasDerivAt
Cleared hypotheses: hff'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have hgg'₁ : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, HasDerivAt g (g' x) x
Tactic: replace hgg' := h.mp <| hgg'.mono fun _ h ↦ h.hasDerivAt
Cleared hypotheses: hgg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have inl : ∀ (hs_Iio : s ∩ Iio a = ∅), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have inr : ∀ (hs_Iio : (s ∩ Iio a).Nonempty), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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 = ∅
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have inl : ∀ (hs_Ioi : s ∩ Ioi a = ∅), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have inl₁ : ∀ (hs_Ioi : (s ∩ Ioi a).Nonempty), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have inr : ∀ (hs_Ioi : s ∩ Ioi a = ∅), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have inr₁ : ∀ (hs_Ioi : (s ∩ Ioi a).Nonempty), 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have 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
Tactic: simp_rw [hs.nhdsWithin_diff_eq_nhdsGT has hs_Iio hs_Ioi] at *
Cleared hypotheses: hg', hfa, hga, hdiv, h, hff', hgg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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 = ∅
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have 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
Tactic: simp_rw [hs.nhdsWithin_diff_eq_nhdsLT has hs_Iio hs_Ioi] at *
Cleared hypotheses: hg', hfa, hga, hdiv, h, hff', hgg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[s \ {a}] a) l
have 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
Tactic: simp_rw [hs.nhdsWithin_diff_eq_nhdsNE has hs_Iio hs_Ioi] at *
Cleared hypotheses: hg', hfa, hga, hdiv, h, hff', hgg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
have hff'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt f (f' x) x
Tactic: apply @lhopital_zero_nhdsNE _ _ _ f' _ g'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hgg'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, HasDerivAt g (g' x) x
Tactic: apply @lhopital_zero_nhdsNE _ _ _ f' _ g'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hg'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, g' x ≠ 0
Tactic: apply @lhopital_zero_nhdsNE _ _ _ f' _ g'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hfa₁ : Tendsto f (𝓝[≠] a) (𝓝 0)
Tactic: apply @lhopital_zero_nhdsNE _ _ _ f' _ g'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hga₁ : Tendsto g (𝓝[≠] a) (𝓝 0)
Tactic: apply @lhopital_zero_nhdsNE _ _ _ f' _ g'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l
have hdiv₁ : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[≠] a) l
Tactic: apply @lhopital_zero_nhdsNE _ _ _ f' _ g'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have hff'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt f (f' y) y
Tactic: rw [eventually_iff_exists_mem] at *
Cleared hypotheses: hff', hgg', hg', hftop, hgtop, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have hgg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, HasDerivAt g (g' y) y
Tactic: rw [eventually_iff_exists_mem] at *
Cleared hypotheses: hff', hgg', hg', hftop, hgtop, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have hg'₁ : ∃ (v : Set ℝ), Membership.mem (γ := Filter ℝ) atTop v ∧ ∀ y ∈ v, g' y ≠ 0
Tactic: rw [eventually_iff_exists_mem] at *
Cleared hypotheses: hff', hgg', hg', hftop, hgtop, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have 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
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 ℝ) 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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have 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
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 ℝ) 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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have rcases : ∀ (s₃ : Set ℝ) (hs₃ : Membership.mem (γ := Filter ℝ) atTop s₃) (hg' : ∀ y ∈ s₃, g' y ≠ 0),
  Tendsto (fun (x : ℝ) ↦ f x / g x) atTop 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' : ℝ → ℝ
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₃
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have hs : Membership.mem (γ := Filter ℝ) atTop s
Tactic: have hs : s ∈ atTop := inter_mem (inter_mem hs₁ hs₂) hs₃
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have hs₄ : ∃ (a : ℝ), ∀ b ≥ a, b ∈ s
Tactic: rw [mem_atTop_sets] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have rcases : ∀ (l_1 : ℝ) (hl : ∀ b ≥ l_1, b ∈ s), Tendsto (fun (x : ℝ) ↦ f x / g x) atTop 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' : ℝ → ℝ
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l_1
have hl' : Ioi l ⊆ s
Tactic: have hl' : Ioi 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' : ℝ → ℝ
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
have refine_1 : ∀ x ∈ Ioi l, HasDerivAt f (f' x) x
Tactic: refine lhopital_zero_atTop_on_Ioi ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hftop hgtop hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l_1
have refine_2 : ∀ x ∈ Ioi l, HasDerivAt g (g' x) x
Tactic: refine lhopital_zero_atTop_on_Ioi ?_ ?_ (fun x hx ↦ hg' x (hl' hx).2) hftop hgtop hdiv