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:

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₀)) := X: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₀)) All 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) := 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)⊢ (∀ 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. 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) 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 := 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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:ℝhx:x ∈ Set.Ioc a bthis:g x = 0⊢ False 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:ℝthis:g x = 0hx:a < x ∧ x ≤ b⊢ False 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:ℝthis✝:g x = 0hx:a < x ∧ x ≤ bthis:?_mvar.59717 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ Falsea:ℝ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 ba:ℝ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 ba:ℝ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: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⊢ Falsea:ℝ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 ba:ℝ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 ba:ℝ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: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⊢ Falsea:ℝ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 ba:ℝ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 ba:ℝ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: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:_fvar.60008 ∈ Set.Icc _fvar.4271 _fvar.4272 := ?_mvar.61846⊢ Falsea:ℝ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 ba:ℝ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 ba:ℝ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 ba:ℝ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: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:_fvar.60008 ∈ Set.Icc _fvar.4271 _fvar.4272 := ?_mvar.61846hgnon:g' y ≠ 0⊢ Falsea:ℝ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 ba:ℝ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 ba:ℝ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 ba:ℝ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) 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⊢ Falsea:ℝ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 ba:ℝ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 ba:ℝ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 ba:ℝ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:DifferentiableWithinAt ℝ g (Set.Icc a b) y⊢ Falsea:ℝ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 ba:ℝ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 ba:ℝ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 ba:ℝ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 := 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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; 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⊢ Set.Ioo a x ⊆ Set.Icc a b; All goals completed! 🐙 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 _fvar.4276 (@_fvar.4278 _fvar.62000) (Set.Ioo _fvar.4271 _fvar.61997) _fvar.62000 := ?_mvar.63115hd:?_mvar.66110 := Chapter10.derivative_unique ?_mvar.66113 _fvar.63116 _fvar.62001⊢ Falsea:ℝ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 _fvar.4276 (@_fvar.4278 _fvar.62000) (Set.Ioo _fvar.4271 _fvar.61997) _fvar.62000 := ?_mvar.63115⊢ ClusterPt y (Filter.principal (Set.Ioo a x \ {y}))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:ℝ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 ba:ℝ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 ba:ℝ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 ba:ℝ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 _fvar.4276 (@_fvar.4278 _fvar.62000) (Set.Ioo _fvar.4271 _fvar.61997) _fvar.62000 := ?_mvar.63115hd:?_mvar.66110 := Chapter10.derivative_unique ?_mvar.66113 _fvar.63116 _fvar.62001⊢ False All goals completed! 🐙 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 _fvar.4276 (@_fvar.4278 _fvar.62000) (Set.Ioo _fvar.4271 _fvar.61997) _fvar.62000 := ?_mvar.63115⊢ 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 _fvar.4276 (@_fvar.4278 _fvar.62000) (Set.Ioo _fvar.4271 _fvar.61997) _fvar.62000 := ?_mvar.63115⊢ Set.Ioo a y ⊆ Set.Ioo a x \ {y}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:ℝ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 ba:ℝ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 ba:ℝ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 ba:ℝ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 _fvar.4276 (@_fvar.4278 _fvar.62000) (Set.Ioo _fvar.4271 _fvar.61997) _fvar.62000 := ?_mvar.63115⊢ ClusterPt y (Filter.principal (Set.Ioo a y)) All goals completed! 🐙 all_goals All goals completed! 🐙 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hx⊢ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hx⊢ ∀ (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)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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hx⊢ 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hx⊢ ∀ (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) 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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) := 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yn have hdiff : DifferentiableOn ℝ 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) All goals completed! 🐙 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhx:∀ (n : ℕ), x n ∈ Set.Ioc a bhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon:ContinuousOn h (Set.Icc a b)⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yn 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon: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; 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon: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 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yna:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yna:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yna:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ h a = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457hb:@_fvar.84237 (@_fvar.83912 _fvar.83923) = 0 := ?_mvar.91489⊢ ∃ yn ∈ Set.Ioo a (x n), f (x n) / g (x n) = f' yn / g' yna:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457⊢ h (x n) = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ h a = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon: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 (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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx this => have this_1 := HasDerivWithinAt.exist_zero (Eq.mp Set.mem_Ioc._simp_1 hx).left (ContinuousOn.mono _fvar.57488 (Filter.Tendsto.of_div'._proof_5 _fvar.4286 _fvar.55943 _fvar.57488 x this (Eq.mp Set.mem_Ioc._simp_1 hx))) (DifferentiableOn.mono _fvar.4280 (Filter.Tendsto.of_div'._proof_6 _fvar.4286 _fvar.55943 _fvar.57488 x this (Eq.mp Set.mem_Ioc._simp_1 hx))) (Filter.Tendsto.of_div'._proof_7 _fvar.4284 _fvar.4286 _fvar.55943 _fvar.57488 x this (Eq.mp Set.mem_Ioc._simp_1 hx)); (fun y x_1 => have this_2 := Filter.Tendsto.of_div'._proof_4 _fvar.4286 _fvar.55943 _fvar.57488 x this (Eq.mp Set.mem_Ioc._simp_1 hx) y x_1.right (Eq.mp Set.mem_Ioo._simp_1 x_1.left); have hg := Eq.mpr (id (congrArg (fun _a => HasDerivWithinAt _fvar.4276 (_a y) (Set.Ioo _fvar.4271 x) y) _fvar.4282)) (HasDerivWithinAt.mono (DifferentiableWithinAt.hasDerivWithinAt (Eq.mp (congrArg (fun _a => _a) (DifferentiableOn.eq_1 ℝ _fvar.4276 (Set.Icc _fvar.4271 _fvar.4272))) _fvar.4280 y this_2)) (Filter.Tendsto.of_div'._proof_2 _fvar.4286 _fvar.55943 _fvar.57488 x this (Eq.mp Set.mem_Ioc._simp_1 hx) y x_1.right (Eq.mp Set.mem_Ioo._simp_1 x_1.left) this_2 (@_fvar.4285 y this_2) (Eq.mp (congrArg (fun _a => _a) (DifferentiableOn.eq_1 ℝ _fvar.4276 (Set.Icc _fvar.4271 _fvar.4272))) _fvar.4280 y this_2))); have hd := Chapter10.derivative_unique (ClusterPt.mono (of_eq_true (Eq.trans Filter.Tendsto.of_div'._simp_2 (Eq.trans (Eq.trans (congrArg (fun x => y ∈ x) (closure_Ioo (have this := Not.intro fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.4271) (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul y (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.4271 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (y ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.4271) (Mathlib.Tactic.Ring.atom_pf y) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul y (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.4271 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (y ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.4271 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul y (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1))))))) Mathlib.Tactic.Ring.neg_zero))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.4271 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero y (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.lt_of_lt_of_eq (Mathlib.Tactic.Linarith.sub_neg_of_lt (Eq.mp Set.mem_Ioo._simp_1 x_1.left).left) (neg_eq_zero.mpr (sub_eq_zero_of_eq a)))); this))) Set.mem_Icc._simp_1) (Eq.trans (congr (congrArg And (eq_true (le_of_lt (Eq.mp Set.mem_Ioo._simp_1 x_1.left).left))) (le_refl._simp_1 y)) (and_self True))))) (Filter.principal_mono.mpr (Filter.Tendsto.of_div'._proof_3 _fvar.4286 _fvar.55943 _fvar.57488 x this (Eq.mp Set.mem_Ioc._simp_1 hx) y x_1.right (Eq.mp Set.mem_Ioo._simp_1 x_1.left) this_2 (@_fvar.4285 y this_2) hg))) hg x_1.right; False.elim (@_fvar.4285 y this_2 hd)) (Classical.choose this_1) (Classical.choose_spec this_1)x:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457hb:@_fvar.84237 (@_fvar.83912 _fvar.83923) = 0 := ?_mvar.91489⊢ h a = h (x n) All goals completed! 🐙) 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457hb:@_fvar.84237 (@_fvar.83912 _fvar.83923) = 0 := ?_mvar.91489yn:ℝ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' yna:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457⊢ h (x n) = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ h a = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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' yna:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457⊢ h (x n) = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ h a = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon: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 := 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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; 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 All goals completed! 🐙 have h2 : HasDerivWithinAt g (g' yn) (.Ioo a (x n)) yn := 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497⊢ HasDerivWithinAt g (derivWithin g (Set.Icc a b) 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497⊢ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497⊢ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497⊢ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497⊢ yn ∈ Set.Icc a b All goals completed! 🐙 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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' yna:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457⊢ h (x n) = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ h a = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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' yna:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457⊢ h (x n) = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ h a = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon: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 := 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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; All goals completed! 🐙 have h6 : f' yn * g (x n) - g' yn * f (x n) = 0 := 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802⊢ ClusterPt yn (Filter.principal (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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802⊢ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802⊢ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802⊢ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802⊢ a ≤ yn; All goals completed! 🐙 All goals completed! 🐙 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802h6:@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248) = 0 := ?_mvar.127142h7:@_fvar.4276 (@_fvar.94246 _fvar.94248) ≠ 0 := ?_mvar.142089⊢ f (x n) / g (x n) = f' yn / g' yna:ℝ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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802h6:@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248) = 0 := ?_mvar.127142⊢ g (x n) ≠ 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457⊢ h (x n) = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ h a = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ 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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802h6:@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248) = 0 := ?_mvar.127142h7:@_fvar.4276 (@_fvar.94246 _fvar.94248) ≠ 0 := ?_mvar.142089h8:@_fvar.4278 _fvar.94255 ≠ 0 := ?_mvar.142121⊢ f (x n) / g (x n) = f' yn / g' yna:ℝ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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802h6:@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248) = 0 := ?_mvar.127142h7:@_fvar.4276 (@_fvar.94246 _fvar.94248) ≠ 0 := ?_mvar.142089⊢ g' yn ≠ 0a:ℝ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' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.94246 _fvar.94248)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 _fvar.4275 (@_fvar.4277 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.95497h2:HasDerivWithinAt _fvar.4276 (@_fvar.4278 _fvar.94255) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.103370h3: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 _fvar.94249 (@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248)) (Set.Ioo _fvar.4271 (@_fvar.94246 _fvar.94248)) _fvar.94255 := ?_mvar.124802h6:@_fvar.4277 _fvar.94255 * @_fvar.4276 (@_fvar.94246 _fvar.94248) - @_fvar.4278 _fvar.94255 * @_fvar.4275 (@_fvar.94246 _fvar.94248) = 0 := ?_mvar.127142⊢ g (x n) ≠ 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385ha:@_fvar.84237 _fvar.4271 = 0 := ?_mvar.91457⊢ h (x n) = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Ioo _fvar.4271 (@_fvar.83912 _fvar.83923)) := DifferentiableOn.mono _fvar.84999 ?_mvar.91385⊢ h a = 0a:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hx:a < x n ∧ x n ≤ bhcon:ContinuousOn _fvar.84237 (Set.Icc _fvar.4271 (@_fvar.83912 _fvar.83923)) := ContinuousOn.mono _fvar.88991 ?_mvar.91263⊢ Set.Ioo a (x n) ⊆ Set.Icc a ba:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝhconv:Filter.Tendsto x Filter.atTop (nhds a)n:ℕh:ℝ → ℝ := fun x' => @_fvar.4275 x' * @_fvar.4276 (@_fvar.83912 _fvar.83923) - @_fvar.4276 x' * @_fvar.4275 (@_fvar.83912 _fvar.83923)hdiff:DifferentiableOn ℝ _fvar.84237 (Set.Icc _fvar.4271 _fvar.4272) := ?_mvar.84998hcon:ContinuousOn h (Set.Icc a b)hx:a < x n ∧ x n ≤ b⊢ Set.Icc a (x n) ⊆ Set.Icc a b all_goals All goals completed! 🐙 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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) := 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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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) ≤ ya:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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) ≤ ya:ℝ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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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 (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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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✝; All goals completed! 🐙) replace hy : ∀ n, y n ∈ Set.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)⊢ (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧ Filter.Tendsto (fun x => f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) All goals completed! 🐙 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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 _fvar.162520 Filter.atTop (nhds _fvar.4271) := ?_mvar.162712hy:∀ (n : ℕ), @_fvar.162520 n ∈ Set.Icc _fvar.4271 _fvar.4272 := ?_mvar.168811⊢ Filter.Tendsto (fun n => f' (y n) / g' (y n)) Filter.atTop (nhds L); 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hxx:ℕ → ℝ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 _fvar.162520 Filter.atTop (nhds _fvar.4271) := ?_mvar.162712hy:∀ (n : ℕ), @_fvar.162520 n ∈ Set.Icc _fvar.4271 _fvar.4272 := ?_mvar.168811⊢ Filter.Tendsto y Filter.atTop (nhdsWithin a (Set.Icc a b)) All goals completed! 🐙 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 _fvar.4271 _fvar.4272, @_fvar.4276 x ≠ 0 := fun x hx => @?_mvar.57675 x hx⊢ a ≤ b; All goals completed! 🐙
end Chapter10