awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
hdnf₁ : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hdng₁ : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
Tactic: rw [neg_Iio] at hdnf hdng
Cleared hypotheses: hdnf, hdng
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have this : Tendsto (fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) atTop l
Tactic: have := lhopital_zero_atTop_on_Ioi hdnf hdng (by grind)
    (hfbot.comp tendsto_neg_atTop_atBot) (hgbot.comp tendsto_neg_atTop_atBot)
    (by simpa using hdiv.comp tendsto_neg_atTop_atBot)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this : Tendsto (fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have this₁ : Tendsto (α := ℝ) ((fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) atBot l
Tactic: have := this.comp tendsto_neg_atBot_atTop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, 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 ∈ Ioo a b, DifferentiableAt ℝ f x
Tactic: have hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x := fun x hx =>
    (hdf x hx).differentiableAt (Ioo_mem_nhds hx.1 hx.2)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf_1 : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, 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 ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
Tactic: have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x := fun x hx =>
    by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : f a = 0
hga : 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 refine_1 : Tendsto f (𝓝[>] a) (𝓝 0)
Tactic: refine lhopital_zero_right_on_Ioo hab hdf hg' ?_ ?_ hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[>] a) l
refine_1 : Tendsto f (𝓝[>] a) (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have refine_2 : Tendsto g (𝓝[>] a) (𝓝 0)
Tactic: refine lhopital_zero_right_on_Ioo hab hdf hg' ?_ ?_ hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[>] a) l
⊢ Tendsto f (𝓝[>] a) (𝓝 0)
have refine_1 : Tendsto f (𝓝[Ioo a b] a) (𝓝 (f a))
Tactic: rw [← hfa, ← nhdsWithin_Ioo_eq_nhdsGT hab]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[>] a) l
⊢ Tendsto g (𝓝[>] a) (𝓝 0)
have refine_2 : Tendsto g (𝓝[Ioo a b] a) (𝓝 (g a))
Tactic: rw [← hga, ← nhdsWithin_Ioo_eq_nhdsGT hab]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[<] b) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have hdf₁ : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
Tactic: have hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x := fun x hx =>
    (hdf x hx).differentiableAt (Ioo_mem_nhds hx.1 hx.2)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hab : a < b
hdf_1 : DifferentiableOn ℝ f (Ioo a b)
hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[<] b) l
hdf : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
Tactic: have hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x := fun x hx =>
    by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioi a)
hg' : ∀ x ∈ Ioi a, 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 hdf₁ : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x
Tactic: have hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x := fun x hx =>
    (hdf x hx).differentiableAt (Ioi_mem_nhds hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf_1 : DifferentiableOn ℝ f (Ioi a)
hg' : ∀ x ∈ Ioi a, 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
hdf : ∀ x ∈ Ioi a, DifferentiableAt ℝ f x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x
Tactic: have hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x := fun x hx =>
    by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Iio a)
hg' : ∀ x ∈ Iio a, 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 hdf₁ : ∀ x ∈ Iio a, DifferentiableAt ℝ f x
Tactic: have hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x := fun x hx =>
    (hdf x hx).differentiableAt (Iio_mem_nhds hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf_1 : DifferentiableOn ℝ f (Iio a)
hg' : ∀ x ∈ Iio a, 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
hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x
Tactic: have hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x := fun x hx =>
    by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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'₁ : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt f (f' y) y
Tactic: rw [eventually_iff_exists_mem] 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' : ℝ → ℝ
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have hgg'₁ : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
Tactic: rw [eventually_iff_exists_mem] 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' : ℝ → ℝ
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have hg'₁ : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
Tactic: rw [eventually_iff_exists_mem] at *
Cleared hypotheses: hff', hgg', hg', hfa, hga, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have rcases : ∀ (s₁ : Set ℝ) (hs₁ : s₁ ∈ 𝓝[>] a) (hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y),
  Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
Tactic: rcases hff' with ⟨s₁, hs₁, hff'⟩
Cleared hypotheses: hff'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have rcases : ∀ (s₂ : Set ℝ) (hs₂ : s₂ ∈ 𝓝[>] a) (hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y),
  Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
Tactic: rcases hgg' with ⟨s₂, hs₂, hgg'⟩
Cleared hypotheses: hgg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have rcases : ∀ (s₃ : Set ℝ) (hs₃ : s₃ ∈ 𝓝[>] a) (hg' : ∀ y ∈ s₃, g' y ≠ 0), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
Tactic: rcases hg' with ⟨s₃, hs₃, hg'⟩
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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₃
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have hs : s ∈ 𝓝[>] a
Tactic: have hs : s ∈ 𝓝[>] a := inter_mem (inter_mem hs₁ hs₂) hs₃
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have hs₄ : ∃ u ∈ Ioi a, Ioo a u ⊆ s
Tactic: rw [mem_nhdsGT_iff_exists_Ioo_subset] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have rcases : ∀ (u : ℝ) (hau : u ∈ Ioi a) (hu : Ioo a u ⊆ s), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
Tactic: rcases hs with ⟨u, hau, hu⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
have refine_1 : ∀ x ∈ Ioo a u, HasDerivAt f (f' x) x
Tactic: refine lhopital_zero_right_on_Ioo hau ?_ ?_ ?_ hfa hga hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have refine_2 : ∀ x ∈ Ioo a u, HasDerivAt g (g' x) x
Tactic: refine lhopital_zero_right_on_Ioo hau ?_ ?_ ?_ hfa hga hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have refine_3 : ∀ x ∈ Ioo a u, g' x ≠ 0
Tactic: refine lhopital_zero_right_on_Ioo hau ?_ ?_ ?_ hfa hga hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt f (f' y) y
Tactic: rw [eventually_iff_exists_mem] 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' : ℝ → ℝ
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
have hgg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, HasDerivAt g (g' y) y
Tactic: rw [eventually_iff_exists_mem] 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' : ℝ → ℝ
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
have hg'₁ : ∃ v ∈ 𝓝[<] a, ∀ y ∈ v, g' y ≠ 0
Tactic: rw [eventually_iff_exists_mem] at *
Cleared hypotheses: hff', hgg', hg', hfa, hga, hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
have rcases : ∀ (s₁ : Set ℝ) (hs₁ : s₁ ∈ 𝓝[<] a) (hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y),
  Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
Tactic: rcases hff' with ⟨s₁, hs₁, hff'⟩
Cleared hypotheses: hff'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
have rcases : ∀ (s₂ : Set ℝ) (hs₂ : s₂ ∈ 𝓝[<] a) (hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y),
  Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
Tactic: rcases hgg' with ⟨s₂, hs₂, hgg'⟩
Cleared hypotheses: hgg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
have rcases : ∀ (s₃ : Set ℝ) (hs₃ : s₃ ∈ 𝓝[<] a) (hg' : ∀ y ∈ s₃, g' y ≠ 0), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
Tactic: rcases hg' with ⟨s₃, hs₃, hg'⟩
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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₃
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
have hs : s ∈ 𝓝[<] a
Tactic: have hs : s ∈ 𝓝[<] a := inter_mem (inter_mem hs₁ hs₂) hs₃
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
have hs₄ : ∃ l ∈ Iio a, Ioo l a ⊆ s
Tactic: rw [mem_nhdsLT_iff_exists_Ioo_subset] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
have rcases : ∀ (l_1 : ℝ) (hal : l_1 ∈ Iio a) (hl : Ioo l_1 a ⊆ s), Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l
Tactic: rcases hs with ⟨l, hal, hl⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
have refine_1 : ∀ x ∈ Ioo l a, HasDerivAt f (f' x) x
Tactic: refine lhopital_zero_left_on_Ioo hal ?_ ?_ ?_ hfa hga hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l_1
have refine_2 : ∀ x ∈ Ioo l a, HasDerivAt g (g' x) x
Tactic: refine lhopital_zero_left_on_Ioo hal ?_ ?_ ?_ hfa hga hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l_1
have refine_3 : ∀ x ∈ Ioo l a, g' x ≠ 0
Tactic: refine lhopital_zero_left_on_Ioo hal ?_ ?_ ?_ hfa hga hdiv