case refine'_1
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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x) (𝓝[Iio b] b) (𝓝 0)

case refine'_2
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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => g x) (𝓝[Iio b] b) (𝓝 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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g 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
refine' lhopital_zero_left_on_Ioo hab hff' hgg' hg' _ _ hdiv
case refine'_1
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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x) (𝓝[Ioo a b] b) (𝓝 (f b))
case refine'_1
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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x) (𝓝[Iio b] b) (𝓝 0)
rw [← hfb, ← nhdsWithin_Ioo_eq_nhdsWithin_Iio hab]
no goals
case refine'_1
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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => f x) (𝓝[Ioo a b] b) (𝓝 (f b))
exact ((hcf b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto
case refine'_2
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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => g x) (𝓝[Ioo a b] b) (𝓝 (g b))
case refine'_2
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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => g x) (𝓝[Iio b] b) (𝓝 0)
rw [← hgb, ← nhdsWithin_Ioo_eq_nhdsWithin_Iio hab]
no goals
case refine'_2
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
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Iio b] b) l
⊢ Tendsto (fun x => g x) (𝓝[Ioo a b] b) (𝓝 (g b))
exact ((hcg b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto