a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ -Ioo a b → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
have hdnf : ∀ x ∈ -Ioo a b, 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 ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ -Ioo a b → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ -Ioo a b → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ -Ioo a b → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
have hdng : ∀ x ∈ -Ioo a b, 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 ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ -Ioo a b → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ -Ioo a b → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ -Ioo a b → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
rw [preimage_neg_Ioo] at hdnf
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ -Ioo a b → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
rw [preimage_neg_Ioo] at hdng
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[Ioi (-b)] (-b)) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
have := lhopital_zero_right_on_Ioo (neg_lt_neg hab) hdnf hdng (by
  intro x hx h
  apply hg' _ (by rw [← preimage_neg_Ioo] at hx; exact hx)
  rwa [mul_comm, ← neg_eq_neg_one_mul, neg_eq_zero] at h)
  (hfb.comp tendsto_neg_nhdsWithin_Ioi_neg) (hgb.comp tendsto_neg_nhdsWithin_Ioi_neg)
  (by
    simp only [neg_div_neg_eq, mul_one, mul_neg]
    exact (tendsto_congr fun x => rfl).mp (hdiv.comp tendsto_neg_nhdsWithin_Ioi_neg))
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this✝ : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[Ioi (-b)] (-b)) l
this : Tendsto ((fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[Ioi (-b)] (-b)) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
have := this.comp tendsto_neg_nhdsWithin_Iio
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this✝ : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[Ioi (-b)] (-b)) l
this : Tendsto (fun x => (fun x => f (-x) / g (-x)) (-x)) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this✝ : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[Ioi (-b)] (-b)) l
this : Tendsto ((fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
unfold Function.comp at this
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this✝ : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[Ioi (-b)] (-b)) l
this : Tendsto (fun x => (fun x => f (-x) / g (-x)) (-x)) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio b] b) l
simpa only [neg_neg]
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioo (-b) (-a)
h : g' (-x) * -1 = 0
⊢ False
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → g' (-x) * -1 ≠ 0
intro x hx h
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioo (-b) (-a)
h : g' (-x) * -1 = 0
⊢ g' (-x) = 0
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioo (-b) (-a)
h : g' (-x) * -1 = 0
⊢ False
apply hg' _ (by rw [← preimage_neg_Ioo] at hx; exact hx)
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioo (-b) (-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 ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx✝ : x ∈ Ioo (-b) (-a)
hx : x ∈ -Ioo a b
h : g' (-x) * -1 = 0
⊢ ?m.13646 h ∈ Ioo a b
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx : x ∈ Ioo (-b) (-a)
h : g' (-x) * -1 = 0
⊢ ?m.13575 ∈ Ioo a b
rw [← preimage_neg_Ioo] at hx
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
x : ℝ
hx✝ : x ∈ Ioo (-b) (-a)
hx : x ∈ -Ioo a b
h : g' (-x) * -1 = 0
⊢ ?m.13646 h ∈ Ioo a b
exact hx
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f' (-x) / g' (-x)) (𝓝[Ioi (-b)] (-b)) ?m.13206
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f' (-x) * -1 / (g' (-x) * -1)) (𝓝[Ioi (-b)] (-b)) ?m.13206
simp only [neg_div_neg_eq, mul_one, mul_neg]
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 0)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
hdnf : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ (x : ℝ), x ∈ Ioo (-b) (-a) → HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun x => f' (-x) / g' (-x)) (𝓝[Ioi (-b)] (-b)) ?m.13206
exact (tendsto_congr fun x => rfl).mp (hdiv.comp tendsto_neg_nhdsWithin_Ioi_neg)