awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
this : Tendsto (fun (x : ℝ) ↦ (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[>] 0) l
⊢ Tendsto (α := ℝ) ((fun (x : ℝ) ↦ (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) ∘ fun (r : ℝ) ↦ r⁻¹) atTop l

Tactic:
have := this.comp tendsto_inv_atTop_nhdsGT_zero
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
this_1 : Tendsto (fun (x : ℝ) ↦ (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[>] 0) l
this : Tendsto (fun (x : ℝ) ↦ (fun (x : ℝ) ↦ f x⁻¹ / g x⁻¹) ((fun (r : ℝ) ↦ r⁻¹) x)) atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
simpa only [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x

Tactic:
have hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x := fun x hx =>
    comp x (hff' (-x) hx) (hasDerivAt_neg x)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x

Tactic:
have hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x := fun x hx =>
    comp x (hgg' (-x) hx) (hasDerivAt_neg x)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x

Tactic:
rw [neg_Iio] at hdnf hdng

Premises used: Set.neg_Iio
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x

Tactic:
rw [neg_Iio] at hdnf hdng

Premises used: Set.neg_Iio
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ x ∈ Ioi (-a), g' (-x) * -1 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.LHopital
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) * -1 / (g' (-x) * -1)) atTop l

Tactic:
simpa using hdiv.comp tendsto_neg_atTop_atBot

Premises used: Filter.tendsto_neg_atTop_atBot, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.LHopital
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 ∘ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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 ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) atBot l

Tactic:
have := this.comp tendsto_neg_atBot_atTop
-- Module: Mathlib.Analysis.Calculus.LHopital
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_1 : Tendsto (fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) atTop l
this : Tendsto (fun (x : ℝ) ↦ (fun (x : ℝ) ↦ f (-x) / g (-x)) (-x)) atBot l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l

Tactic:
simpa only [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
HasDerivAt.lhopital_zero_right_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfa hga hdiv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.lhopital_zero_right_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
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
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
exact HasDerivAt.lhopital_zero_right_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfa hga hdiv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.lhopital_zero_right_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
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

Tactic:
lhopital_zero_right_on_Ioo hab hdf hg' ?_ ?_ hdiv

Premises used: deriv.lhopital_zero_right_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
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)
refine_2 : Tendsto g (𝓝[>] a) (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
refine lhopital_zero_right_on_Ioo hab hdf hg' ?_ ?_ hdiv

Premises used: deriv.lhopital_zero_right_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
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 (𝓝[Ioo a b] a) (𝓝 (f a))
⊢ Tendsto f (𝓝[>] a) (𝓝 0)

Tactic:
rw [← hfa, ← nhdsWithin_Ioo_eq_nhdsGT hab]

Premises used: nhdsWithin_Ioo_eq_nhdsGT
-- Module: Mathlib.Analysis.Calculus.LHopital
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 (𝓝[Ioo a b] a) (𝓝 (f a))

Tactic:
((hcf a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto

Premises used: Iff.mpr, Set.left_mem_Ico, Set.Ioo_subset_Ico_self, ContinuousWithinAt.mono, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
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 (𝓝[Ioo a b] a) (𝓝 (f a))

Tactic:
exact ((hcf a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto

Premises used: Iff.mpr, Set.left_mem_Ico, Set.Ioo_subset_Ico_self, ContinuousWithinAt.mono, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
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_2 : Tendsto g (𝓝[Ioo a b] a) (𝓝 (g a))
⊢ Tendsto g (𝓝[>] a) (𝓝 0)

Tactic:
rw [← hga, ← nhdsWithin_Ioo_eq_nhdsGT hab]

Premises used: nhdsWithin_Ioo_eq_nhdsGT
-- Module: Mathlib.Analysis.Calculus.LHopital
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 (𝓝[Ioo a b] a) (𝓝 (g a))

Tactic:
((hcg a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto

Premises used: Iff.mpr, Set.left_mem_Ico, Set.Ioo_subset_Ico_self, ContinuousWithinAt.mono, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
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 (𝓝[Ioo a b] a) (𝓝 (g a))

Tactic:
exact ((hcg a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto

Premises used: Iff.mpr, Set.left_mem_Ico, Set.Ioo_subset_Ico_self, ContinuousWithinAt.mono, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l

Tactic:
HasDerivAt.lhopital_zero_left_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfb hgb hdiv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.lhopital_zero_left_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
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
hdg : ∀ x ∈ Ioo a b, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l

Tactic:
exact HasDerivAt.lhopital_zero_left_on_Ioo hab (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfb hgb hdiv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.lhopital_zero_left_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
HasDerivAt.lhopital_zero_atTop_on_Ioi (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hftop hgtop hdiv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.lhopital_zero_atTop_on_Ioi
-- Module: Mathlib.Analysis.Calculus.LHopital
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
hdg : ∀ x ∈ Ioi a, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
exact HasDerivAt.lhopital_zero_atTop_on_Ioi (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hftop hgtop hdiv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.lhopital_zero_atTop_on_Ioi
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.LHopital
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
hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l

Tactic:
HasDerivAt.lhopital_zero_atBot_on_Iio (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfbot hgbot hdiv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.lhopital_zero_atBot_on_Iio
-- Module: Mathlib.Analysis.Calculus.LHopital
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
hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l

Tactic:
exact HasDerivAt.lhopital_zero_atBot_on_Iio (fun x hx => (hdf x hx).hasDerivAt)
    (fun x hx => (hdg x hx).hasDerivAt) hg' hfbot hgbot hdiv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.lhopital_zero_atBot_on_Iio
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
⊢ ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt f (f' y) y

Tactic:
rw [eventually_iff_exists_mem] at *

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

Tactic:
rw [eventually_iff_exists_mem] at *

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

Tactic:
rw [eventually_iff_exists_mem] at *

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

Tactic:
rw [eventually_iff_exists_mem] at *

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

Tactic:
rw [eventually_iff_exists_mem] at *

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

Tactic:
rw [eventually_iff_exists_mem] at *

Premises used: Filter.eventually_iff_exists_mem