Analysis
10.5. L'Hôpital's rule

Imports

import Mathlib.Tactic
import Analysis.Section_9_1
import Analysis.Section_10_1
import Analysis.Section_10_2

Analysis I, Section 10.5: L'Hôpital's rule

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

L'Hôpital's rule.

open Chapter9namespace Chapter10

Proposition 10.5.1 (L'Hôpital's rule, I) / Exercise 10.5.1

theorem declaration uses `sorry`_root_.Filter.Tendsto.of_div {X: Set ℝ} {f g: ℝ → ℝ} {x₀ f'x₀ g'x₀:ℝ}
  (hfx₀: f x₀ = 0) (hgx₀: g x₀ = 0) (hg_non: g'x₀ ≠ 0)
  (hf'x₀: HasDerivWithinAt f f'x₀ X x₀) (hg'x₀: HasDerivWithinAt g g'x₀ X x₀) :
  (∃ δ > 0, ∀ x ∈ X \ {x₀} ∩ .Ioo (x₀ - δ) (x₀ + δ), g x ≠ 0) ∧
  (nhdsWithin x₀ (X \ {x₀})).Tendsto (fun x ↦ f x / g x) (nhds (f'x₀ / g'x₀))
  := byX:Set ℝf:ℝ → ℝg:ℝ → ℝx₀:ℝf'x₀:ℝg'x₀:ℝhfx₀:f x₀ = 0hgx₀:g x₀ = 0hg_non:g'x₀ ≠ 0hf'x₀:HasDerivWithinAt f f'x₀ X x₀hg'x₀:HasDerivWithinAt g g'x₀ X x₀⊢ (∃ δ > 0, ∀ x ∈ X \ {x₀} ∩ Set.Ioo (x₀ - δ) (x₀ + δ), g x ≠ 0) ∧
  Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin x₀ (X \ {x₀})) (nhds (f'x₀ / g'x₀))
  sorryAll goals completed! 🐙

Proposition 10.5.2 (L'Hôpital's rule, II)

theorem _root_.Filter.Tendsto.of_div' {a b L:ℝ} (hab: a < b) {f g f' g': ℝ → ℝ}
  (hf: DifferentiableOn ℝ f (.Icc a b)) (hg: DifferentiableOn ℝ g (.Icc a b))
  (hf': f' = derivWithin f (.Icc a b)) (hg': g' = derivWithin g (.Icc a b))
  (hfa: f a = 0) (hga: g a = 0) (hgnon: ∀ x ∈ Set.Icc a b, g' x ≠ 0)
  (hderiv: (nhdsWithin a (.Icc a b)).Tendsto (fun x ↦ f' x / g' x) (nhds L)) :
  (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧
  (nhdsWithin a (.Ioc a b)).Tendsto (fun x ↦ f x / g x) (nhds L) := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
  -- This proof is written to follow the structure of the original text.
  observe hfcon : ContinuousOn f (.Icc a b)a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
  observe hgcon : ContinuousOn g (.Icc a b)a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
  have (x:ℝ) (hx: x ∈ Set.Ioc a b) : g x ≠ 0 := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
    by_contra thisa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝhx:x ∈ Set.Ioc a bthis:g x = 0⊢ False
    simp at hxa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ False
    have := HasDerivWithinAt.exist_zero hx.1 (hgcon.mono ?_) (hg.mono ?_) ?_refine_4a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ bthis:∃ x_1 ∈ Set.Ioo a x, HasDerivWithinAt g 0 (Set.Ioo a x) x_1⊢ Falserefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x
    choose y hy hgy using thisrefine_4a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ by:ℝhy:y ∈ Set.Ioo a xhgy:HasDerivWithinAt g 0 (Set.Ioo a x) y⊢ Falserefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x; simp at hyrefine_4a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < x⊢ Falserefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x
    have : y ∈ Set.Icc a b := ?_refine_4.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a b⊢ Falserefine_4.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < x⊢ y ∈ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x
    specialize hgnon y thisrefine_4.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0⊢ Falserefine_4.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < x⊢ y ∈ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x
    rw [DifferentiableOn.eq_1] at hf hgrefine_4.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0⊢ Falserefine_4.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < x⊢ y ∈ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x; specialize hg y thisrefine_4.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:DifferentiableWithinAt ℝ g (Set.Icc a b) y⊢ Falserefine_4.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < x⊢ y ∈ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x
    replace hg : HasDerivWithinAt g (g' y) (.Ioo a x) y := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
      rw [hg']a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:DifferentiableWithinAt ℝ g (Set.Icc a b) y⊢ HasDerivWithinAt g (derivWithin g (Set.Icc a b) y) (Set.Ioo a x) y; apply hg.hasDerivWithinAt.monoa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:DifferentiableWithinAt ℝ g (Set.Icc a b) y⊢ Set.Ioo a x ⊆ Set.Icc a b; grindAll goals completed! 🐙
    have hd := derivative_unique ?_ hg hgyrefine_4.refine_2.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:HasDerivWithinAt g (g' y) (Set.Ioo a x) yhd:g' y = 0⊢ Falserefine_4.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:HasDerivWithinAt g (g' y) (Set.Ioo a x) y⊢ ClusterPt y (Filter.principal (Set.Ioo a x \ {y}))refine_4.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < x⊢ y ∈ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x
    .refine_4.refine_2.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:HasDerivWithinAt g (g' y) (Set.Ioo a x) yhd:g' y = 0⊢ False contradictionAll goals completed! 🐙
    apply ClusterPt.mono _ ((Filter.principal_mono (s := .Ioo a y)).mpr  _)a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:HasDerivWithinAt g (g' y) (Set.Ioo a x) y⊢ ClusterPt y (Filter.principal (Set.Ioo a y))a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:HasDerivWithinAt g (g' y) (Set.Ioo a x) y⊢ Set.Ioo a y ⊆ Set.Ioo a x \ {y}refine_4.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < x⊢ y ∈ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Icc a x ⊆ Set.Icc a brefine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ Set.Ioo a x ⊆ Set.Icc a brefine_3a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ g a = g x
    .a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)x:ℝthis✝:g x = 0hx:a < x ∧ x ≤ by:ℝhgy:HasDerivWithinAt g 0 (Set.Ioo a x) yhy:a < y ∧ y < xthis:y ∈ Set.Icc a bhgnon:g' y ≠ 0hg:HasDerivWithinAt g (g' y) (Set.Ioo a x) y⊢ ClusterPt y (Filter.principal (Set.Ioo a y)) simp [←mem_closure_iff_clusterPt, closure_Ioo (show a ≠ y by linarith), le_of_lt hy.1]All goals completed! 🐙
    all_goals grindAll goals completed! 🐙
  refine ⟨ this, ?_ ⟩a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0⊢ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
  rw [←Convergesto.iff, Convergesto.iff_conv]a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0⊢ ∀ (a_1 : ℕ → ℝ),
  (∀ (n : ℕ), a_1 n ∈ Set.Ioc a b) →
    Filter.Tendsto a_1 Filter.atTop (nhds a) → Filter.Tendsto (fun n ↦ f (a_1 n) / g (a_1 n)) Filter.atTop (nhds L)ha:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0⊢ AdherentPt a (Set.Ioc a b)
  .a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0⊢ ∀ (a_1 : ℕ → ℝ),
  (∀ (n : ℕ), a_1 n ∈ Set.Ioc a b) →
    Filter.Tendsto a_1 Filter.atTop (nhds a) → Filter.Tendsto (fun n ↦ f (a_1 n) / g (a_1 n)) Filter.atTop (nhds L) intro x hxa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a b⊢ Filter.Tendsto x Filter.atTop (nhds a) → Filter.Tendsto (fun n ↦ f (x n) / g (x n)) Filter.atTop (nhds L) hconva:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)⊢ Filter.Tendsto (fun n ↦ f (x n) / g (x n)) Filter.atTop (nhds L)
    have hxy (n:ℕ) : ∃ yn ∈ Set.Ioo a (x n), (f (x n))/(g (x n)) = f' yn / (g' yn) := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
      set h : ℝ → ℝ := fun x' ↦ (f x') * (g (x n)) - (g x') * (f (x n))a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yn
      have hdiff : DifferentiableOn ℝ h (.Icc a b) := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) fun_propAll goals completed! 🐙
      observe hcon : ContinuousOn h (.Icc a b)a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yn
      specialize hx na:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:x n ∈ Set.Ioc a b⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yn; simp at hxa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yn
      replace hcon : ContinuousOn h (.Icc a (x n)) := hcon.mono ?_refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' ynrefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      replace hdiff : DifferentiableOn ℝ h (.Ioo a (x n)) := hdiff.mono ?_refine_2.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' ynrefine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      have ha : h a = 0 := ?_refine_2.refine_2.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' ynrefine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ h a = 0refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      have hb : h (x n) = 0 := ?_refine_2.refine_2.refine_2.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' ynrefine_2.refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0⊢ h (x n) = 0refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ h a = 0refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      choose yn hyn hdh using HasDerivWithinAt.exist_zero hx.1 hcon hdiff (bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0⊢ h a = h (x n) grindAll goals completed! 🐙)
      use yn, hynrighta:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) yn⊢ f (x n) / g (x n) = f' yn / g' ynrefine_2.refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0⊢ h (x n) = 0refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ h a = 0refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      rw [DifferentiableOn.eq_1] at hf hgrighta:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) yn⊢ f (x n) / g (x n) = f' yn / g' ynrefine_2.refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0⊢ h (x n) = 0refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ h a = 0refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      have h1 : HasDerivWithinAt f (f' yn) (.Ioo a (x n)) yn := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
        rw [hf']a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) yn⊢ HasDerivWithinAt f (derivWithin f (Set.Icc a b) yn) (Set.Ioo a (x n)) yn; apply (hf _ _).hasDerivWithinAt.monoa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) yn⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) yn⊢ yn ∈ Set.Icc a b <;>a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) yn⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) yn⊢ yn ∈ Set.Icc a b grindAll goals completed! 🐙
      have h2 : HasDerivWithinAt g (g' yn) (.Ioo a (x n)) yn := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
        rw [hg']a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) yn⊢ HasDerivWithinAt g (derivWithin g (Set.Icc a b) yn) (Set.Ioo a (x n)) yn; apply (hg _ _).hasDerivWithinAt.monoa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) yn⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) yn⊢ yn ∈ Set.Icc a b <;>a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) yn⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) yn⊢ yn ∈ Set.Icc a b grindAll goals completed! 🐙
      observe h3 : HasDerivWithinAt (fun x' ↦ (f x') * (g (x n))) ((f' yn)*(g (x n))) (.Ioo a (x n)) ynrighta:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) yn⊢ f (x n) / g (x n) = f' yn / g' ynrefine_2.refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0⊢ h (x n) = 0refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ h a = 0refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      observe h4 : HasDerivWithinAt (fun x' ↦ (g x') * (f (x n))) ((g' yn)*(f (x n))) (.Ioo a (x n)) ynrighta:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) yn⊢ f (x n) / g (x n) = f' yn / g' ynrefine_2.refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0⊢ h (x n) = 0refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ h a = 0refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      have h5 : HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (.Ioo a (x n)) yn := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
        simp [h]a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) yn⊢ HasDerivWithinAt (fun x' ↦ f x' * g (x n) - g x' * f (x n)) (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) yn; exact h3.sub h4All goals completed! 🐙
      have h6 : f' yn * g (x n) - g' yn * f (x n) = 0 := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
        apply derivative_unique _ h5 hdha:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) yn⊢ ClusterPt yn (Filter.principal (Set.Ioo a (x n) \ {yn}))
        apply ClusterPt.mono _ ((Filter.principal_mono (s := .Ioo a yn)).mpr  _)a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) yn⊢ ClusterPt yn (Filter.principal (Set.Ioo a yn))a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) yn⊢ Set.Ioo a yn ⊆ Set.Ioo a (x n) \ {yn}
        .a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) yn⊢ ClusterPt yn (Filter.principal (Set.Ioo a yn)) simp [←mem_closure_iff_clusterPt, closure_Ioo (show a ≠ yn by grind)]a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) yn⊢ a ≤ yn; grindAll goals completed! 🐙
        grindAll goals completed! 🐙
      have h7 : g (x n) ≠ 0 := ?_right.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) ynh6:f' yn * g (x n) - g' yn * f (x n) = 0h7:g (x n) ≠ 0⊢ f (x n) / g (x n) = f' yn / g' ynright.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) ynh6:f' yn * g (x n) - g' yn * f (x n) = 0⊢ g (x n) ≠ 0refine_2.refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0⊢ h (x n) = 0refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ h a = 0refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      have h8 : g' (yn) ≠ 0 := ?_right.refine_2.refine_2a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) ynh6:f' yn * g (x n) - g' yn * f (x n) = 0h7:g (x n) ≠ 0h8:g' yn ≠ 0⊢ f (x n) / g (x n) = f' yn / g' ynright.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) ynh6:f' yn * g (x n) - g' yn * f (x n) = 0h7:g (x n) ≠ 0⊢ g' yn ≠ 0right.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ f (Set.Icc a b) xhg:∀ x ∈ Set.Icc a b, DifferentiableWithinAt ℝ g (Set.Icc a b) xhf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0hb:h (x n) = 0yn:ℝhyn:yn ∈ Set.Ioo a (x n)hdh:HasDerivWithinAt h 0 (Set.Ioo a (x n)) ynh1:HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) ynh2:HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) ynh3:HasDerivWithinAt (fun y ↦ f y * g (x n)) (f' yn * g (x n)) (Set.Ioo a (x n)) ynh4:HasDerivWithinAt (fun y ↦ g y * f (x n)) (g' yn * f (x n)) (Set.Ioo a (x n)) ynh5:HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) ynh6:f' yn * g (x n) - g' yn * f (x n) = 0⊢ g (x n) ≠ 0refine_2.refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))ha:h a = 0⊢ h (x n) = 0refine_2.refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))hdiff:DifferentiableOn ℝ h (Set.Ioo a (x n))⊢ h a = 0refine_2.refine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn h (Set.Icc a (x n))⊢ Set.Ioo a (x n) ⊆ Set.Icc a brefine_1a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' ↦ f x' * g (x n) - g x' * f (x n)hdiff:DifferentiableOn ℝ h (Set.Icc a b)hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b
      all_goals grindAll goals completed! 🐙
    choose y hy hy' using hxya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Ioo a (x n)hy':∀ (n : ℕ), f (x n) / g (x n) = f' (y n) / g' (y n)⊢ Filter.Tendsto (fun n ↦ f (x n) / g (x n)) Filter.atTop (nhds L)
    have hyconv : Filter.atTop.Tendsto y (nhds a) := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L)
      apply tendsto_const_nhds.squeeze hconvhgfa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Ioo a (x n)hy':∀ (n : ℕ), f (x n) / g (x n) = f' (y n) / g' (y n)⊢ (fun x ↦ a) ≤ yhfha:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Ioo a (x n)hy':∀ (n : ℕ), f (x n) / g (x n) = f' (y n) / g' (y n)⊢ y ≤ x <;>hgfa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Ioo a (x n)hy':∀ (n : ℕ), f (x n) / g (x n) = f' (y n) / g' (y n)⊢ (fun x ↦ a) ≤ yhfha:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Ioo a (x n)hy':∀ (n : ℕ), f (x n) / g (x n) = f' (y n) / g' (y n)⊢ y ≤ x (intro _hfha:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Set.Ioo a (x n)hy':∀ (n : ℕ), f (x n) / g (x n) = f' (y n) / g' (y n)i✝:ℕ⊢ y i✝ ≤ x i✝; grindAll goals completed! 🐙)
    replace hy : ∀ n, y n ∈ Set.Icc a b := bya:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) grindAll goals completed! 🐙
    simp_rw [a:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)y:ℕ → ℝhy':∀ (n : ℕ), f (x n) / g (x n) = f' (y n) / g' (y n)hyconv:Filter.Tendsto y Filter.atTop (nhds a)hy:∀ (n : ℕ), y n ∈ Set.Icc a b⊢ Filter.Tendsto (fun n ↦ f (x n) / g (x n)) Filter.atTop (nhds L)hy']; apply hderiv.compa:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)y:ℕ → ℝhy':∀ (n : ℕ), f (x n) / g (x n) = f' (y n) / g' (y n)hyconv:Filter.Tendsto y Filter.atTop (nhds a)hy:∀ (n : ℕ), y n ∈ Set.Icc a b⊢ Filter.Tendsto y Filter.atTop (nhdsWithin a (Set.Icc a b))
    solve_by_elim [tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within,
    Filter.Eventually.of_forall]All goals completed! 🐙
  simp [←closure_def', closure_Ioc (show a ≠ b by grind)]ha:ℝb:ℝL:ℝhab:a < bf:ℝ → ℝg:ℝ → ℝf':ℝ → ℝg':ℝ → ℝhf:DifferentiableOn ℝ f (Set.Icc a b)hg:DifferentiableOn ℝ g (Set.Icc a b)hf':f' = derivWithin f (Set.Icc a b)hg':g' = derivWithin g (Set.Icc a b)hfa:f a = 0hga:g a = 0hgnon:∀ x ∈ Set.Icc a b, g' x ≠ 0hderiv:Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)hfcon:ContinuousOn f (Set.Icc a b)hgcon:ContinuousOn g (Set.Icc a b)this:∀ x ∈ Set.Ioc a b, g x ≠ 0⊢ a ≤ b; grindAll goals completed! 🐙

end Chapter10