awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
simp : Tendsto (fun (x : ℝ) ↦ f' (-x) / g' (-x)) (𝓝[>] (-b)) l
⊢ Tendsto (fun (x : ℝ) ↦ f' (-x) * -1 / (g' (-x) * -1)) (𝓝[>] (-b)) l

Tactic:
simp only [neg_div_neg_eq, mul_one, mul_neg]

Premises used: neg_div_neg_eq, mul_one, mul_neg
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f' (-x) / g' (-x)) (𝓝[>] (-b)) l

Tactic:
hdiv.comp tendsto_neg_nhdsGT_neg

Premises used: tendsto_neg_nhdsGT_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f' (-x) / g' (-x)) (𝓝[>] (-b)) l

Tactic:
exact hdiv.comp tendsto_neg_nhdsGT_neg

Premises used: tendsto_neg_nhdsGT_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[>] (-b)) l

Tactic:
have := lhopital_zero_right_on_Ioo (neg_lt_neg hab) hdnf hdng (by grind)
    (hfb.comp tendsto_neg_nhdsGT_neg) (hgb.comp tendsto_neg_nhdsGT_neg)
    (by
      simp only [neg_div_neg_eq, mul_one, mul_neg]
      exact hdiv.comp tendsto_neg_nhdsGT_neg)
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this : Tendsto (fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[>] (-b)) l
⊢ Tendsto ((fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) (𝓝[<] b) l

Tactic:
have := this.comp tendsto_neg_nhdsLT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this_1 : Tendsto (fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[>] (-b)) l
this : Tendsto (fun (x : ℝ) ↦ (fun (x : ℝ) ↦ f (-x) / g (-x)) (-x)) (𝓝[<] b) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l

Tactic:
simpa only [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l

Tactic:
lhopital_zero_left_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv

Premises used: HasDerivAt.lhopital_zero_left_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
refine_1 : Tendsto f (𝓝[<] b) (𝓝 0)
refine_2 : Tendsto g (𝓝[<] b) (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l

Tactic:
refine lhopital_zero_left_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv

Premises used: HasDerivAt.lhopital_zero_left_on_Ioo
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
refine_1 : Tendsto f (𝓝[Ioo a b] b) (𝓝 (f b))
⊢ Tendsto f (𝓝[<] b) (𝓝 0)

Tactic:
rw [← hfb, ← nhdsWithin_Ioo_eq_nhdsLT hab]

Premises used: nhdsWithin_Ioo_eq_nhdsLT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 (f b))

Tactic:
((hcf b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto

Premises used: Iff.mpr, ContinuousWithinAt.mono, Set.Ioo_subset_Ioc_self, Set.right_mem_Ioc, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 (f b))

Tactic:
exact ((hcf b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto

Premises used: Iff.mpr, ContinuousWithinAt.mono, Set.Ioo_subset_Ioc_self, Set.right_mem_Ioc, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
refine_2 : Tendsto g (𝓝[Ioo a b] b) (𝓝 (g b))
⊢ Tendsto g (𝓝[<] b) (𝓝 0)

Tactic:
rw [← hgb, ← nhdsWithin_Ioo_eq_nhdsLT hab]

Premises used: nhdsWithin_Ioo_eq_nhdsLT
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto g (𝓝[Ioo a b] b) (𝓝 (g b))

Tactic:
((hcg b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto

Premises used: Iff.mpr, ContinuousWithinAt.mono, Set.Ioo_subset_Ioc_self, Set.right_mem_Ioc, ContinuousWithinAt.tendsto
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto g (𝓝[Ioo a b] b) (𝓝 (g b))

Tactic:
exact ((hcg b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto

Premises used: Iff.mpr, ContinuousWithinAt.mono, Set.Ioo_subset_Ioc_self, Set.right_mem_Ioc, ContinuousWithinAt.tendsto
-- 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' : ℝ), a < a' ∧ 0 < a'

Tactic:
⟨1 + max a 0,
    ⟨lt_of_le_of_lt (le_max_left a 0) (lt_one_add _),
      lt_of_le_of_lt (le_max_right a 0) (lt_one_add _)⟩⟩

Premises used: le_max_right, lt_of_le_of_lt, HAdd.hAdd, Max.max, And.intro, Exists.intro, OfNat.ofNat, le_max_left, lt_one_add
-- 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
obtain : ∀ (a' : ℝ) (haa' : a < a') (ha' : 0 < a'), Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
obtain ⟨a', haa', ha'⟩ : ∃ a', a < a' ∧ 0 < a' := ⟨1 + max a 0,
    ⟨lt_of_le_of_lt (le_max_left a 0) (lt_one_add _),
      lt_of_le_of_lt (le_max_right a 0) (lt_one_add _)⟩⟩
-- 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'
⊢ ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0

Tactic:
have fact1 : ∀ x : ℝ, x ∈ Ioo 0 a'⁻¹ → x ≠ 0 := fun _ hx => (ne_of_lt hx.1).symm
-- 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
⊢ ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹

Tactic:
have fact2 (x) (hx : x ∈ Ioo 0 a'⁻¹) : a < x⁻¹ := lt_trans haa' ((lt_inv_comm₀ ha' hx.1).mpr hx.2)
-- 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⁻¹
⊢ ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x

Tactic:
have hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x := fun x hx =>
    comp x (hff' x⁻¹ <| fact2 x hx) (hasDerivAt_inv <| fact1 x hx)
-- 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
⊢ ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x

Tactic:
have hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x := fun x hx =>
    comp x (hgg' x⁻¹ <| fact2 x hx) (hasDerivAt_inv <| fact1 x hx)
-- 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
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
⊢ g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ ≠ 0

Tactic:
mul_ne_zero ?_ (neg_ne_zero.mpr <| inv_ne_zero <| pow_ne_zero _ <| fact1 x hx)

Premises used: Iff.mpr, pow_ne_zero, neg_ne_zero, inv_ne_zero, mul_ne_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
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
refine : g' x⁻¹ ≠ 0
⊢ g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ ≠ 0

Tactic:
refine mul_ne_zero ?_ (neg_ne_zero.mpr <| inv_ne_zero <| pow_ne_zero _ <| fact1 x hx)

Premises used: Iff.mpr, pow_ne_zero, neg_ne_zero, inv_ne_zero, mul_ne_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
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
⊢ g' x⁻¹ ≠ 0

Tactic:
hg' _ (fact2 x hx)
-- 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
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
⊢ g' x⁻¹ ≠ 0

Tactic:
exact hg' _ (fact2 x hx)
-- 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
⊢ Tendsto (fun (x : ℝ) ↦ f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)) (𝓝[>] 0) l

Tactic:
(tendsto_congr' ?_).mp (hdiv.comp tendsto_inv_nhdsGT_zero)

Premises used: tendsto_inv_nhdsGT_zero, Iff.mp, Filter.Tendsto.comp, Filter.tendsto_congr'
-- 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
refine :
  EventuallyEq (β := ℝ) (𝓝[>] 0) ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) fun (x : ℝ) ↦
    f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
⊢ Tendsto (fun (x : ℝ) ↦ f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)) (𝓝[>] 0) l

Tactic:
refine (tendsto_congr' ?_).mp (hdiv.comp tendsto_inv_nhdsGT_zero)

Premises used: tendsto_inv_nhdsGT_zero, Iff.mp, Filter.Tendsto.comp, Filter.tendsto_congr'
-- 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
x : ℝ
h :
  ∀ (hx : 0 < x),
    ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) x =
      f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x →
    ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) x =
      f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
(hx : 0 < x)
-- 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
h :
  ∀ (x : ℝ) (hx : 0 < x),
    ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) x =
      f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
⊢ EventuallyEq (β := ℝ) (𝓝[>] 0) ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) fun (x : ℝ) ↦
    f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
filter_upwards [self_mem_nhdsWithin] with x (hx : 0 < x)

Premises used: self_mem_nhdsWithin
-- 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
x : ℝ
hx : 0 < x
h : f' x⁻¹ / g' x⁻¹ = f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
⊢ ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) x =
    f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
simp only [Function.comp_def]

Premises used: Function.comp_def
-- 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
x : ℝ
hx : 0 < x
h : -(HPow.hPow (β := ℕ) x 2)⁻¹ ≠ 0
⊢ f' x⁻¹ / g' x⁻¹ = f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
rw [mul_div_mul_right]

Premises used: mul_div_mul_right
-- 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
x : ℝ
hx : 0 < x
⊢ (HPow.hPow (β := ℕ) x 2)⁻¹ ≠ 0

Tactic:
positivity
-- 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
x : ℝ
hx : 0 < x
⊢ -(HPow.hPow (β := ℕ) x 2)⁻¹ ≠ 0

Tactic:
exact neg_ne_zero.mpr (by positivity)

Premises used: Iff.mpr, neg_ne_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
⊢ Tendsto (fun (x : ℝ) ↦ (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[>] 0) l

Tactic:
have := lhopital_zero_right_on_Ioo (inv_pos.mpr ha') hdnf hdng
    (by
      intro x hx
      refine mul_ne_zero ?_ (neg_ne_zero.mpr <| inv_ne_zero <| pow_ne_zero _ <| fact1 x hx)
      exact hg' _ (fact2 x hx))
    (hftop.comp tendsto_inv_nhdsGT_zero) (hgtop.comp tendsto_inv_nhdsGT_zero)
    (by
      refine (tendsto_congr' ?_).mp (hdiv.comp tendsto_inv_nhdsGT_zero)
      filter_upwards [self_mem_nhdsWithin] with x (hx : 0 < x)
      simp only [Function.comp_def]
      rw [mul_div_mul_right]
      exact neg_ne_zero.mpr (by positivity))