-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_left_on_Ioc (hab : a < b) (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x)
    (hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x) (hcf : ContinuousOn f (Ioc a b))
    (hcg : ContinuousOn g (Ioc a b)) (hg' : ∀ x ∈ Ioo a b, g' x ≠ 0) (hfb : f b = 0) (hgb : g b = 0)
    (hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l) :
    Tendsto (fun x => f x / g x) (𝓝[<] b) l

Proof state:
case refine_1
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto f (𝓝[<] b) (𝓝 0)

Tactic:
rw [← hfb, ← nhdsWithin_Ioo_eq_nhdsLT hab]

Result:
case refine_1
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 (f b))

Proof state:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto (fun x => f x / g x) (𝓝[<] b) l

Tactic:
refine lhopital_zero_left_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv

Result:
case refine_1
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto f (𝓝[<] b) (𝓝 0)

case refine_2
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto g (𝓝[<] b) (𝓝 0)

Proof state:
case refine_2
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto g (𝓝[Ioo a b] b) (𝓝 (g b))

Tactic:
exact ((hcg b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto

Result:
no goals

Proof state:
case refine_1
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 (f b))

Tactic:
exact ((hcf b <| right_mem_Ioc.mpr hab).mono Ioo_subset_Ioc_self).tendsto

Result:
no goals

Proof state:
case refine_2
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto g (𝓝[<] b) (𝓝 0)

Tactic:
rw [← hgb, ← nhdsWithin_Ioo_eq_nhdsLT hab]

Result:
case refine_2
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[<] b) l
⊢ Tendsto g (𝓝[Ioo a b] b) (𝓝 (g b))