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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
have sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b := fun x hx =>
  Ioo_subset_Ioo (le_refl a) (le_of_lt hx.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
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
have hg : ∀ x ∈ Ioo a b, g x ≠ 0 := by
  intro x hx h
  have : Tendsto g (𝓝[<] x) (𝓝 0) := by
    rw [← h, ← nhdsWithin_Ioo_eq_nhdsWithin_Iio hx.1]
    exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto
  obtain ⟨y, hyx, hy⟩ : ∃ c ∈ Ioo a x, g' c = 0
  exact exists_hasDerivAt_eq_zero' hx.1 hga this fun y hy => hgg' y <| sub x hx hy
  exact hg' y (sub x hx hyx) hy
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
this : ∀ (x : ℝ), x ∈ Ioo a b → ∃ c, c ∈ Ioo a x ∧ f x * g' c = g x * f' c
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
have : ∀ x ∈ Ioo a b, ∃ c ∈ Ioo a x, f x * g' c = g x * f' c := by
  intro x hx
  rw [← sub_zero (f x), ← sub_zero (g x)]
  exact exists_ratio_hasDerivAt_eq_ratio_slope' g g' hx.1 f f' (fun y hy => hgg' y <| sub x hx hy)
    (fun y hy => hff' y <| sub x hx hy) hga hfa
    (tendsto_nhdsWithin_of_tendsto_nhds (hgg' x hx).continuousAt.tendsto)
    (tendsto_nhdsWithin_of_tendsto_nhds (hff' x hx).continuousAt.tendsto)
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
this : ∀ (x : ℝ), x ∈ Ioo a b → ∃ c, c ∈ Ioo a x ∧ f x * g' c = g x * f' c
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
choose! c hc using this
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
have : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x := by
  intro x hx
  rcases hc x hx with ⟨h₁, h₂⟩
  field_simp [hg x hx, hg' (c x) ((sub x hx) h₁)]
  simp only [h₂]
  rw [mul_comm]
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
have cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x := fun x hx => (hc x hx).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
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioo a b] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioi a] a) l
rw [← nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab]
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto (fun x => ((fun x' => f' x' / g' x') ∘ c) x) (𝓝[Ioo a b] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto (fun x => f x / g x) (𝓝[Ioo a b] a) l
apply tendsto_nhdsWithin_congr this
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto (fun x => ((fun x' => f' x' / g' x') ∘ c) x) (𝓝[Ioo a b] a) 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto (fun x => ((fun x' => f' x' / g' x') ∘ c) x) (𝓝[Ioo a b] a) l
simp only
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto c (𝓝[Ioo a b] a) (𝓝[Ioi a] a)
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto (fun x => ((fun x' => f' x' / g' x') ∘ c) x) (𝓝[Ioo a b] a) l
apply hdiv.comp
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
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, a ≤ c 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
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, c b ≤ id b

case refine'_3
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ᶠ (x : ℝ) in 𝓝[Ioo a b] a, c x ∈ Ioi a
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ Tendsto c (𝓝[Ioo a b] a) (𝓝[Ioi a] a)
refine' tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
  (tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
    (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id) _ _) _
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
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, a ≤ c 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
hg' : ∀ (x : ℝ), x ∈ Ioo a b → g' x ≠ 0
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, c b ≤ id b

case refine'_3
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ᶠ (x : ℝ) in 𝓝[Ioo a b] a, c x ∈ Ioi a
all_goals
  apply eventually_nhdsWithin_of_forall
  intro x hx
  have := cmp x hx
  try simp
  linarith [this]
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
⊢ ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[Iio x] x) (𝓝 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ False
have : Tendsto g (𝓝[<] x) (𝓝 0) := by
  rw [← h, ← nhdsWithin_Ioo_eq_nhdsWithin_Iio hx.1]
  exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[Iio x] x) (𝓝 0)
⊢ ∃ c, c ∈ Ioo a x ∧ g' c = 0

case intro.intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[Iio x] x) (𝓝 0)
y : ℝ
hyx : y ∈ Ioo a x
hy : g' y = 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[Iio x] x) (𝓝 0)
⊢ False
obtain ⟨y, hyx, hy⟩ : ∃ c ∈ Ioo a x, g' c = 0
case intro.intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[Iio x] x) (𝓝 0)
y : ℝ
hyx : y ∈ Ioo a x
hy : g' y = 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[Iio x] x) (𝓝 0)
⊢ ∃ c, c ∈ Ioo a x ∧ g' c = 0

case intro.intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[Iio x] x) (𝓝 0)
y : ℝ
hyx : y ∈ Ioo a x
hy : g' y = 0
⊢ False
exact exists_hasDerivAt_eq_zero' hx.1 hga this fun y hy => hgg' y <| sub x hx hy
no goals
case intro.intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[Iio x] x) (𝓝 0)
y : ℝ
hyx : y ∈ Ioo a x
hy : g' y = 0
⊢ False
exact hg' y (sub x hx hyx) hy
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ Tendsto g (𝓝[Ioo a x] x) (𝓝 (g 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ Tendsto g (𝓝[Iio x] x) (𝓝 0)
rw [← h, ← nhdsWithin_Ioo_eq_nhdsWithin_Iio hx.1]
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ Tendsto g (𝓝[Ioo a x] x) (𝓝 (g x))
exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
x : ℝ
hx : x ∈ Ioo a b
⊢ ∃ c, c ∈ Ioo a x ∧ f x * g' c = g x * f' c
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
⊢ ∀ (x : ℝ), x ∈ Ioo a b → ∃ c, c ∈ Ioo a x ∧ f x * g' c = g x * f' c
intro x 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
x : ℝ
hx : x ∈ Ioo a b
⊢ ∃ c, c ∈ Ioo a x ∧ (f x - 0) * g' c = (g x - 0) * f' c
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
x : ℝ
hx : x ∈ Ioo a b
⊢ ∃ c, c ∈ Ioo a x ∧ f x * g' c = g x * f' c
rw [← sub_zero (f x), ← sub_zero (g x)]
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
x : ℝ
hx : x ∈ Ioo a b
⊢ ∃ c, c ∈ Ioo a x ∧ (f x - 0) * g' c = (g x - 0) * f' c
exact exists_ratio_hasDerivAt_eq_ratio_slope' g g' hx.1 f f' (fun y hy => hgg' y <| sub x hx hy)
  (fun y hy => hff' y <| sub x hx hy) hga hfa
  (tendsto_nhdsWithin_of_tendsto_nhds (hgg' x hx).continuousAt.tendsto)
  (tendsto_nhdsWithin_of_tendsto_nhds (hff' x hx).continuousAt.tendsto)
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
x : ℝ
hx : x ∈ Ioo a b
⊢ ((fun x' => f' x' / g' x') ∘ c) x = f x / g 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
⊢ ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
intro x hx
case intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
x : ℝ
hx : x ∈ Ioo a b
h₁ : c x ∈ Ioo a x
h₂ : f x * g' (c x) = g x * f' (c x)
⊢ ((fun x' => f' x' / g' x') ∘ c) x = f x / g 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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
x : ℝ
hx : x ∈ Ioo a b
⊢ ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
rcases hc x hx with ⟨h₁, h₂⟩
case intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
x : ℝ
hx : x ∈ Ioo a b
h₁ : c x ∈ Ioo a x
h₂ : f x * g' (c x) = g x * f' (c x)
⊢ f' (c x) * g x = f x * g' (c x)
case intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
x : ℝ
hx : x ∈ Ioo a b
h₁ : c x ∈ Ioo a x
h₂ : f x * g' (c x) = g x * f' (c x)
⊢ ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
field_simp [hg x hx, hg' (c x) ((sub x hx) h₁)]
case intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
x : ℝ
hx : x ∈ Ioo a b
h₁ : c x ∈ Ioo a x
h₂ : f x * g' (c x) = g x * f' (c x)
⊢ f' (c x) * g x = g x * f' (c x)
case intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
x : ℝ
hx : x ∈ Ioo a b
h₁ : c x ∈ Ioo a x
h₂ : f x * g' (c x) = g x * f' (c x)
⊢ f' (c x) * g x = f x * g' (c x)
simp only [h₂]
no goals
case intro
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
x : ℝ
hx : x ∈ Ioo a b
h₁ : c x ∈ Ioo a x
h₂ : f x * g' (c x) = g x * f' (c x)
⊢ f' (c x) * g x = g x * f' (c x)
rw [mul_comm]
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioi a
case refine'_3
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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ᶠ (x : ℝ) in 𝓝[Ioo a b] a, c x ∈ Ioi a
apply eventually_nhdsWithin_of_forall
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
⊢ c x ∈ Ioi a
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
⊢ ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioi a
intro x hx
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ c x ∈ Ioi a
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
⊢ c x ∈ Ioi a
have := cmp x hx
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ a < c x
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ c x ∈ Ioi a
try simp
no goals
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ a < c x
linarith [this]
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ a < c x
case refine'_3.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
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 0)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[Ioi a] a) l
sub : ∀ (x : ℝ), x ∈ Ioo a b → Ioo a x ⊆ Ioo a b
hg : ∀ (x : ℝ), x ∈ Ioo a b → g x ≠ 0
c : ℝ → ℝ
hc : ∀ (x : ℝ), x ∈ Ioo a b → c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this✝ : ∀ (x : ℝ), x ∈ Ioo a b → ((fun x' => f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ (x : ℝ), x ∈ Ioo a b → a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ c x ∈ Ioi a
simp