ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>f : X → Y<VAR>h : Conformal f<GOAL>Differentiable ℝ f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedAddCommGroup Z<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>NormedSpace ℝ Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Conformal f<VAR>hg : Conformal g<GOAL>Conformal (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedAddCommGroup Y<VAR>NormedSpace ℝ X<VAR>NormedSpace ℝ Y<VAR>f : X → Y<VAR>hf : Conformal f<VAR>c : ℝ<VAR>hc : c ≠ 0<GOAL>Conformal (c • f)
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>a b : E<VAR>f' : ℝ<VAR>l : Filter E<VAR>h : IsExtrFilter f l a<VAR>hd : HasLineDerivAt ℝ f f' a b<VAR>h' : Filter.Tendsto (fun t => a + t • b) (𝓝 0) l<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>a b : E<VAR>l : Filter E<VAR>h : IsExtrFilter f l a<VAR>h' : Filter.Tendsto (fun t => a + t • b) (𝓝 0) l<GOAL>lineDeriv ℝ f a b = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsExtrOn f s a<VAR>hd : HasLineDerivAt ℝ f f' a b<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>h : IsExtrOn f s a<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>lineDeriv ℝ f a b = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsMinOn f s a<VAR>hd : HasLineDerivAt ℝ f f' a b<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>h : IsMinOn f s a<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>lineDeriv ℝ f a b = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsMaxOn f s a<VAR>hd : HasLineDerivAt ℝ f f' a b<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>h : IsMaxOn f s a<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>lineDeriv ℝ f a b = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsExtrOn f s a<VAR>hd : HasLineDerivWithinAt ℝ f f' s a b<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>h : IsExtrOn f s a<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>lineDerivWithin ℝ f s a b = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsMinOn f s a<VAR>hd : HasLineDerivWithinAt ℝ f f' s a b<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>h : IsMinOn f s a<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>lineDerivWithin ℝ f s a b = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsMaxOn f s a<VAR>hd : HasLineDerivWithinAt ℝ f f' s a b<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>a b : E<VAR>h : IsMaxOn f s a<VAR>h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s<GOAL>lineDerivWithin ℝ f s a b = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>f : E → ℝ<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsLocalExtr f a<VAR>hd : HasLineDerivAt ℝ f f' a b<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>h : IsLocalExtr f a<GOAL>lineDeriv ℝ f a = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>f : E → ℝ<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsLocalMin f a<VAR>hd : HasLineDerivAt ℝ f f' a b<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>h : IsLocalMin f a<GOAL>lineDeriv ℝ f a = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>f : E → ℝ<VAR>a b : E<VAR>f' : ℝ<VAR>h : IsLocalMax f a<VAR>hd : HasLineDerivAt ℝ f f' a b<GOAL>f' = 0
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>f : E → ℝ<VAR>a : E<VAR>h : IsLocalMax f a<GOAL>lineDeriv ℝ f a = 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>hg : HasDerivAtFilter g₁ g₁' (h x) L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hL : Filter.Tendsto h L L'<GOAL>HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hg : HasDerivAtFilter g₁ g₁' y L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hy : y = h x<VAR>hL : Filter.Tendsto h L L'<GOAL>HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>s' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>hg : HasDerivWithinAt g₁ g₁' s' (h x)<VAR>hh : HasDerivAt h h' x<VAR>hs : ∀ (x : 𝕜), h x ∈ s'<GOAL>HasDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>s' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>y : 𝕜'<VAR>hg : HasDerivWithinAt g₁ g₁' s' y<VAR>hh : HasDerivAt h h' x<VAR>hs : ∀ (x : 𝕜), h x ∈ s'<VAR>hy : y = h x<GOAL>HasDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>hg : HasDerivWithinAt g₁ g₁' t' (h x)<VAR>hh : HasDerivWithinAt h h' s x<VAR>hst : Set.MapsTo h s t'<GOAL>HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>y : 𝕜'<VAR>hg : HasDerivWithinAt g₁ g₁' t' y<VAR>hh : HasDerivWithinAt h h' s x<VAR>hst : Set.MapsTo h s t'<VAR>hy : y = h x<GOAL>HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>hg : HasDerivAt g₁ g₁' (h x)<VAR>hh : HasDerivAt h h' x<GOAL>HasDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>y : 𝕜'<VAR>hg : HasDerivAt g₁ g₁' y<VAR>hh : HasDerivAt h h' x<VAR>hy : y = h x<GOAL>HasDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>hg : HasStrictDerivAt g₁ g₁' (h x)<VAR>hh : HasStrictDerivAt h h' x<GOAL>HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>y : 𝕜'<VAR>hg : HasStrictDerivAt g₁ g₁' y<VAR>hh : HasStrictDerivAt h h' x<VAR>hy : y = h x<GOAL>HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>hg : HasDerivAt g₁ g₁' (h x)<VAR>hh : HasDerivWithinAt h h' s x<GOAL>HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>y : 𝕜'<VAR>hg : HasDerivAt g₁ g₁' y<VAR>hh : HasDerivWithinAt h h' s x<VAR>hy : y = h x<GOAL>HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>g₁ : 𝕜' → F<VAR>hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)<VAR>hh : DifferentiableWithinAt 𝕜 h s x<VAR>hs : Set.MapsTo h s t'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>g₁ : 𝕜' → F<VAR>y : 𝕜'<VAR>hg : DifferentiableWithinAt 𝕜' g₁ t' y<VAR>hh : DifferentiableWithinAt 𝕜 h s x<VAR>hs : Set.MapsTo h s t'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hy : y = h x<GOAL>derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>g₁ : 𝕜' → F<VAR>hg : DifferentiableAt 𝕜' g₁ (h x)<VAR>hh : DifferentiableAt 𝕜 h x<GOAL>deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>h : 𝕜 → 𝕜'<VAR>g₁ : 𝕜' → F<VAR>y : 𝕜'<VAR>hg : DifferentiableAt 𝕜' g₁ y<VAR>hh : DifferentiableAt 𝕜 h x<VAR>hy : y = h x<GOAL>deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' : 𝕜'<VAR>L' : Filter 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>L'' : Filter E<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L''<VAR>hL : Filter.Tendsto f L'' L'<GOAL>HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' : 𝕜'<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>L'' : Filter E<VAR>hh₂ : HasDerivAtFilter h₂ h₂' y L'<VAR>hf : HasFDerivAtFilter f f' x L''<VAR>hL : Filter.Tendsto f L'' L'<VAR>hy : y = f x<GOAL>HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>hh : HasStrictDerivAt h₂ h₂' (f x)<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>hh : HasStrictDerivAt h₂ h₂' y<VAR>hf : HasStrictFDerivAt f f' x<VAR>hy : y = f x<GOAL>HasStrictFDerivAt (h₂ ∘ f) (h₂' • f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>hh : HasDerivAt h₂ h₂' (f x)<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (h₂ ∘ f) (h₂' • f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>hh : HasDerivAt h₂ h₂' y<VAR>hf : HasFDerivAt f f' x<VAR>hy : y = f x<GOAL>HasFDerivAt (h₂ ∘ f) (h₂' • f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>s : Set E<VAR>x : E<VAR>hh : HasDerivAt h₂ h₂' (f x)<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>s : Set E<VAR>x : E<VAR>hh : HasDerivAt h₂ h₂' y<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hy : y = f x<GOAL>HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>s : Set E<VAR>t : Set 𝕜'<VAR>x : E<VAR>hh : HasDerivWithinAt h₂ h₂' t (f x)<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hst : Set.MapsTo f s t<GOAL>HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h₂' y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>s : Set E<VAR>t : Set 𝕜'<VAR>x : E<VAR>hh : HasDerivWithinAt h₂ h₂' t y<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hst : Set.MapsTo f s t<VAR>hy : y = f x<GOAL>HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>L' : Filter 𝕜'<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hL : Filter.Tendsto h L L'<GOAL>HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivAtFilter h₂ h₂' y L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hL : Filter.Tendsto h L L'<VAR>hy : y = h x<GOAL>HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>s' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)<VAR>hh : HasDerivWithinAt h h' s x<VAR>hst : Set.MapsTo h s s'<GOAL>HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>s' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' y : 𝕜'<VAR>hh₂ : HasDerivWithinAt h₂ h₂' s' y<VAR>hh : HasDerivWithinAt h h' s x<VAR>hst : Set.MapsTo h s s'<VAR>hy : y = h x<GOAL>HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>hh₂ : HasDerivAt h₂ h₂' (h x)<VAR>hh : HasDerivAt h h' x<GOAL>HasDerivAt (h₂ ∘ h) (h₂' * h') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' y : 𝕜'<VAR>hh₂ : HasDerivAt h₂ h₂' y<VAR>hh : HasDerivAt h h' x<VAR>hy : y = h x<GOAL>HasDerivAt (h₂ ∘ h) (h₂' * h') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>hh₂ : HasStrictDerivAt h₂ h₂' (h x)<VAR>hh : HasStrictDerivAt h h' x<GOAL>HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' y : 𝕜'<VAR>hh₂ : HasStrictDerivAt h₂ h₂' y<VAR>hh : HasStrictDerivAt h h' x<VAR>hy : y = h x<GOAL>HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>hh₂ : HasDerivAt h₂ h₂' (h x)<VAR>hh : HasDerivWithinAt h h' s x<GOAL>HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' y : 𝕜'<VAR>hh₂ : HasDerivAt h₂ h₂' y<VAR>hh : HasDerivWithinAt h h' s x<VAR>hy : y = h x<GOAL>HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>s' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)<VAR>hh : DifferentiableWithinAt 𝕜 h s x<VAR>hs : Set.MapsTo h s s'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>s' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : DifferentiableWithinAt 𝕜' h₂ s' y<VAR>hh : DifferentiableWithinAt 𝕜 h s x<VAR>hs : Set.MapsTo h s s'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hy : y = h x<GOAL>derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>hh₂ : DifferentiableAt 𝕜' h₂ (h x)<VAR>hh : DifferentiableAt 𝕜 h x<GOAL>deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₂ : 𝕜' → 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : DifferentiableAt 𝕜' h₂ y<VAR>hh : DifferentiableAt 𝕜 h x<VAR>hy : y = h x<GOAL>deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasDerivAtFilter f f' x L<VAR>hL : Filter.Tendsto f L L<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasDerivAtFilter f^[n] (f' ^ n) x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasDerivAt f^[n] (f' ^ n) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : Set.MapsTo f s s<VAR>n : ℕ<GOAL>HasDerivWithinAt f^[n] (f' ^ n) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasStrictDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasStrictDerivAt f^[n] (f' ^ n) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>t : Set F<VAR>hl : HasFDerivWithinAt l l' t (f x)<VAR>hf : HasDerivWithinAt f f' s x<VAR>hst : Set.MapsTo f s t<GOAL>HasDerivWithinAt (l ∘ f) (l' f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>t : Set F<VAR>hl : HasFDerivWithinAt l l' t y<VAR>hf : HasDerivWithinAt f f' s x<VAR>hst : Set.MapsTo f s t<VAR>hy : y = f x<GOAL>HasDerivWithinAt (l ∘ f) (l' f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>hl : HasFDerivAt l l' (f x)<VAR>hf : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (l ∘ f) (l' f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>hl : HasFDerivAt l l' y<VAR>hf : HasDerivWithinAt f f' s x<VAR>hy : y = f x<GOAL>HasDerivWithinAt (l ∘ f) (l' f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>hl : HasFDerivAt l l' (f x)<VAR>hf : HasDerivAt f f' x<GOAL>HasDerivAt (l ∘ f) (l' f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>hl : HasFDerivAt l l' y<VAR>hf : HasDerivAt f f' x<VAR>hy : y = f x<GOAL>HasDerivAt (l ∘ f) (l' f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>hl : HasStrictFDerivAt l l' (f x)<VAR>hf : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (l ∘ f) (l' f') x