case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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'
⊢ Tendsto (fun x => f x / g x) atTop l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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
⊢ Tendsto (fun x => f x / g x) atTop l
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 _)⟩⟩
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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'
⊢ Tendsto (fun x => f x / g x) atTop l
have fact1 : ∀ x : ℝ, x ∈ Ioo 0 a'⁻¹ → x ≠ 0 := fun _ hx => (ne_of_lt hx.1).symm
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
⊢ Tendsto (fun x => f x / g x) atTop l
have fact2 : ∀ x ∈ Ioo 0 a'⁻¹, a < x⁻¹ := fun _ hx => lt_trans haa' ((lt_inv ha' hx.1).mpr hx.2)
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
⊢ Tendsto (fun x => f x / g x) atTop l
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)
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ Tendsto (fun x => f x / g x) atTop l
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)
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
this : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[Ioi 0] 0) l
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ Tendsto (fun x => f x / g x) atTop l
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_zero_atTop) (hgtop.comp tendsto_inv_zero_atTop)
  (by
    refine' (tendsto_congr' _).mp (hdiv.comp tendsto_inv_zero_atTop)
    rw [eventuallyEq_iff_exists_mem]
    use Ioi 0, self_mem_nhdsWithin
    intro x hx
    unfold Function.comp
    simp only
    erw [mul_div_mul_right]
    refine' neg_ne_zero.mpr (inv_ne_zero <| pow_ne_zero _ <| ne_of_gt hx))
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
this✝ : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[Ioi 0] 0) l
this : Tendsto ((fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) ∘ fun r => r⁻¹) atTop l
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
this : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[Ioi 0] 0) l
⊢ Tendsto (fun x => f x / g x) atTop l
have := this.comp tendsto_inv_atTop_zero'
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
this✝ : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[Ioi 0] 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
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
this✝ : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[Ioi 0] 0) l
this : Tendsto ((fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) ∘ fun r => r⁻¹) atTop l
⊢ Tendsto (fun x => f x / g x) atTop l
unfold Function.comp at this
no goals
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
this✝ : Tendsto (fun x => (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[Ioi 0] 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
simpa only [inv_inv]
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
⊢ g' x⁻¹ * -(x ^ 2)⁻¹ ≠ 0
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → g' x⁻¹ * -(x ^ 2)⁻¹ ≠ 0
intro x hx
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
⊢ g' x⁻¹ ≠ 0
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
⊢ g' x⁻¹ * -(x ^ 2)⁻¹ ≠ 0
refine' mul_ne_zero _ (neg_ne_zero.mpr <| inv_ne_zero <| pow_ne_zero _ <| fact1 x hx)
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
⊢ g' x⁻¹ ≠ 0
exact hg' _ (fact2 x hx)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ ((fun x => f' x / g' x) ∘ fun x => x⁻¹) =ᶠ[𝓝[Ioi 0] 0] fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ Tendsto (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) (𝓝[Ioi 0] 0) ?m.22156
refine' (tendsto_congr' _).mp (hdiv.comp tendsto_inv_zero_atTop)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ ∃ s,
    s ∈ 𝓝[Ioi 0] 0 ∧
      EqOn ((fun x => f' x / g' x) ∘ fun x => x⁻¹) (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) s
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ ((fun x => f' x / g' x) ∘ fun x => x⁻¹) =ᶠ[𝓝[Ioi 0] 0] fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)
rw [eventuallyEq_iff_exists_mem]
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ EqOn ((fun x => f' x / g' x) ∘ fun x => x⁻¹) (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) (Ioi 0)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ ∃ s,
    s ∈ 𝓝[Ioi 0] 0 ∧
      EqOn ((fun x => f' x / g' x) ∘ fun x => x⁻¹) (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) s
use Ioi 0, self_mem_nhdsWithin
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ ((fun x => f' x / g' x) ∘ fun x => x⁻¹) x = (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) x
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
⊢ EqOn ((fun x => f' x / g' x) ∘ fun x => x⁻¹) (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) (Ioi 0)
intro x hx
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => f' x / g' x) ((fun x => x⁻¹) x) = (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) x
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ ((fun x => f' x / g' x) ∘ fun x => x⁻¹) x = (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) x
unfold Function.comp
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ f' x⁻¹ / g' x⁻¹ = f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => f' x / g' x) ((fun x => x⁻¹) x) = (fun x => f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)) x
simp only
case hc
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ -(x ^ 2)⁻¹ ≠ 0
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ f' x⁻¹ / g' x⁻¹ = f' x⁻¹ * -(x ^ 2)⁻¹ / (g' x⁻¹ * -(x ^ 2)⁻¹)
erw [mul_div_mul_right]
no goals
case hc
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioo 0 a'⁻¹ → x ≠ 0
fact2 : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → a < x⁻¹
hdnf : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x
hdng : ∀ (x : ℝ), x ∈ Ioo 0 a'⁻¹ → HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x
x : ℝ
hx : x ∈ Ioi 0
⊢ -(x ^ 2)⁻¹ ≠ 0
refine' neg_ne_zero.mpr (inv_ne_zero <| pow_ne_zero _ <| ne_of_gt hx)