case refine'_1
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => f x) (𝓝[Ioi a] a) (𝓝 0)

case refine'_2
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => g x) (𝓝[Ioi a] a) (𝓝 0)
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
refine' lhopital_zero_right_on_Ioo hab hdf hg' _ _ hdiv
case refine'_1
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => f x) (𝓝[Ioo a b] a) (𝓝 (f a))
case refine'_1
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => f x) (𝓝[Ioi a] a) (𝓝 0)
rw [← hfa, ← nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab]
no goals
case refine'_1
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => f x) (𝓝[Ioo a b] a) (𝓝 (f a))
exact ((hcf a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto
case refine'_2
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => g x) (𝓝[Ioo a b] a) (𝓝 (g a))
case refine'_2
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => g x) (𝓝[Ioi a] a) (𝓝 0)
rw [← hga, ← nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab]
no goals
case refine'_2
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Ioo a b)
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ (x : ℝ), x ∈ Ioo a b → deriv g x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => g x) (𝓝[Ioo a b] a) (𝓝 (g a))
exact ((hcg a <| left_mem_Ico.mpr hab).mono Ioo_subset_Ico_self).tendsto