a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : (∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt f (f' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[Ioi a] a, HasDerivAt f (f' x) x
hgg' : (∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt g (g' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[Ioi a] a, HasDerivAt g (g' x) x
hg' : (∀ᶠ (x : ℝ) in 𝓝[Iio a] a, g' x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[Ioi a] a, g' x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0) ∧ Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0) ∧ Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio a] a) l ∧ Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l ∧ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝[{a}ᶜ] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[{a}ᶜ] a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[{a}ᶜ] a, g' x ≠ 0
hfa : Tendsto f (𝓝[{a}ᶜ] a) (𝓝 0)
hga : Tendsto g (𝓝[{a}ᶜ] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[{a}ᶜ] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[{a}ᶜ] a) l
simp only [← Iio_union_Ioi, nhdsWithin_union, tendsto_sup, eventually_sup] at *
no goals
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : (∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt f (f' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[Ioi a] a, HasDerivAt f (f' x) x
hgg' : (∀ᶠ (x : ℝ) in 𝓝[Iio a] a, HasDerivAt g (g' x) x) ∧ ∀ᶠ (x : ℝ) in 𝓝[Ioi a] a, HasDerivAt g (g' x) x
hg' : (∀ᶠ (x : ℝ) in 𝓝[Iio a] a, g' x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[Ioi a] a, g' x ≠ 0
hfa : Tendsto f (𝓝[Iio a] a) (𝓝 0) ∧ Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Iio a] a) (𝓝 0) ∧ Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio a] a) l ∧ Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Iio a] a) l ∧ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
exact ⟨lhopital_zero_nhds_left hff'.1 hgg'.1 hg'.1 hfa.1 hga.1 hdiv.1,
  lhopital_zero_nhds_right hff'.2 hgg'.2 hg'.2 hfa.2 hga.2 hdiv.2⟩