a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ -Iio a → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) atBot l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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
⊢ Tendsto (fun x => f x / g x) atBot l
have hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x := fun x hx =>
  comp x (hff' (-x) hx) (hasDerivAt_neg x)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ -Iio a → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ -Iio a → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) atBot l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ -Iio a → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) atBot l
have hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x := fun x hx =>
  comp x (hgg' (-x) hx) (hasDerivAt_neg x)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ -Iio a → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) atBot l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ -Iio a → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ -Iio a → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) atBot l
rw [preimage_neg_Iio] at hdnf
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) atBot l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ -Iio a → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) atBot l
rw [preimage_neg_Iio] at hdng
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), 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
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) atBot l
have := lhopital_zero_atTop_on_Ioi hdnf hdng
  (by
    intro x hx h
    apply hg' _ (by rw [← preimage_neg_Iio] at hx; exact hx)
    rwa [mul_comm, ← neg_eq_neg_one_mul, neg_eq_zero] at h)
  (hfbot.comp tendsto_neg_atTop_atBot) (hgbot.comp tendsto_neg_atTop_atBot)
  (by
    simp only [mul_one, mul_neg, neg_div_neg_eq]
    exact (tendsto_congr fun x => rfl).mp (hdiv.comp tendsto_neg_atTop_atBot))
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), 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
this : Tendsto ((fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) atBot l
⊢ Tendsto (fun x => f x / g x) atBot l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), 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.comp tendsto_neg_atBot_atTop
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), 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
this : Tendsto (fun x => (fun x => f (-x) / g (-x)) (-x)) atBot l
⊢ Tendsto (fun x => f x / g x) atBot l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), 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
this : Tendsto ((fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) atBot l
⊢ Tendsto (fun x => f x / g x) atBot l
unfold Function.comp at this
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), 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
this : Tendsto (fun x => (fun x => f (-x) / g (-x)) (-x)) atBot l
⊢ Tendsto (fun x => f x / g x) atBot l
simpa only [neg_neg]
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioi (-a)
h : g' (-x) * -1 = 0
⊢ False
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ ∀ (x : ℝ), x ∈ Ioi (-a) → g' (-x) * -1 ≠ 0
intro x hx h
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioi (-a)
h : g' (-x) * -1 = 0
⊢ g' (-x) = 0
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioi (-a)
h : g' (-x) * -1 = 0
⊢ False
apply hg' _ (by rw [← preimage_neg_Iio] at hx; exact hx)
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioi (-a)
h : g' (-x) * -1 = 0
⊢ g' (-x) = 0
rwa [mul_comm, ← neg_eq_neg_one_mul, neg_eq_zero] at h
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx✝ : x ∈ Ioi (-a)
hx : x ∈ -Iio a
h : g' (-x) * -1 = 0
⊢ ?m.27141 h ∈ Iio a
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioi (-a)
h : g' (-x) * -1 = 0
⊢ ?m.27057 ∈ Iio a
rw [← preimage_neg_Iio] at hx
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx✝ : x ∈ Ioi (-a)
hx : x ∈ -Iio a
h : g' (-x) * -1 = 0
⊢ ?m.27141 h ∈ Iio a
exact hx
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f' (-x) / g' (-x)) atTop ?m.26894
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f' (-x) * -1 / (g' (-x) * -1)) atTop ?m.26894
simp only [mul_one, mul_neg, neg_div_neg_eq]
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Iio a → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), 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 : ℝ), x ∈ Ioi (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioi (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f' (-x) / g' (-x)) atTop ?m.26894
exact (tendsto_congr fun x => rfl).mp (hdiv.comp tendsto_neg_atTop_atBot)