ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>u : (i : ι) → M i<GOAL>fderivWithin 𝕜 (fun y => (c y) u) s x = (fderivWithin 𝕜 c s x).flipMultilinear u
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>hc : DifferentiableAt 𝕜 c x<VAR>u : (i : ι) → M i<GOAL>fderiv 𝕜 (fun y => (c y) u) x = (fderiv 𝕜 c x).flipMultilinear u
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>u : (i : ι) → M i<VAR>m : E<GOAL>(fderivWithin 𝕜 (fun y => (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>hc : DifferentiableAt 𝕜 c x<VAR>u : (i : ι) → M i<VAR>m : E<GOAL>(fderiv 𝕜 (fun y => (c y) u) x) m = ((fderiv 𝕜 c x) m) u
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasStrictFDerivAt c c' x<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasFDerivAt c c' x<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hf : DifferentiableWithinAt 𝕜 f s x<GOAL>DifferentiableWithinAt 𝕜 (fun y => c y • f y) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (fun y => c y • f y) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : DifferentiableOn 𝕜 c s<VAR>hf : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (fun y => c y • f y) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : Differentiable 𝕜 c<VAR>hf : Differentiable 𝕜 f<GOAL>Differentiable 𝕜 fun y => c y • f y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hf : DifferentiableWithinAt 𝕜 f s x<GOAL>fderivWithin 𝕜 (fun y => c y • f y) s x = c x • fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>fderiv 𝕜 (fun y => c y • f y) x = c x • fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasStrictFDerivAt c c' x<VAR>f : F<GOAL>HasStrictFDerivAt (fun y => c y • f) (c'.smulRight f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>f : F<GOAL>HasFDerivWithinAt (fun y => c y • f) (c'.smulRight f) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>c' : E →L[𝕜] 𝕜'<VAR>hc : HasFDerivAt c c' x<VAR>f : F<GOAL>HasFDerivAt (fun y => c y • f) (c'.smulRight f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>f : F<GOAL>DifferentiableWithinAt 𝕜 (fun y => c y • f) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>f : F<GOAL>DifferentiableAt 𝕜 (fun y => c y • f) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : DifferentiableOn 𝕜 c s<VAR>f : F<GOAL>DifferentiableOn 𝕜 (fun y => c y • f) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : Differentiable 𝕜 c<VAR>f : F<GOAL>Differentiable 𝕜 fun y => c y • f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>f : F<GOAL>fderivWithin 𝕜 (fun y => c y • f) s x = (fderivWithin 𝕜 c s x).smulRight f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' F<VAR>IsScalarTower 𝕜 𝕜' F<VAR>c : E → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>f : F<GOAL>fderiv 𝕜 (fun y => c y • f) x = (fderiv 𝕜 c x).smulRight f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>x : E<VAR>ha : HasStrictFDerivAt a a' x<VAR>hb : HasStrictFDerivAt b b' x<GOAL>HasStrictFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasStrictFDerivAt c c' x<VAR>hd : HasStrictFDerivAt d d' x<GOAL>HasStrictFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>ha : HasFDerivWithinAt a a' s x<VAR>hb : HasFDerivWithinAt b b' s x<GOAL>HasFDerivWithinAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>hd : HasFDerivWithinAt d d' s x<GOAL>HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>ha : HasFDerivAt a a' x<VAR>hb : HasFDerivAt b b' x<GOAL>HasFDerivAt (fun y => a y * b y) (a x • b' + a'.smulRight (b x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivAt c c' x<VAR>hd : HasFDerivAt d d' x<GOAL>HasFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>ha : DifferentiableWithinAt 𝕜 a s x<VAR>hb : DifferentiableWithinAt 𝕜 b s x<GOAL>DifferentiableWithinAt 𝕜 (fun y => a y * b y) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>ha : DifferentiableAt 𝕜 a x<VAR>hb : DifferentiableAt 𝕜 b x<GOAL>DifferentiableAt 𝕜 (fun y => a y * b y) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>ha : DifferentiableOn 𝕜 a s<VAR>hb : DifferentiableOn 𝕜 b s<GOAL>DifferentiableOn 𝕜 (fun y => a y * b y) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>ha : Differentiable 𝕜 a<VAR>hb : Differentiable 𝕜 b<GOAL>Differentiable 𝕜 fun y => a y * b y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableWithinAt 𝕜 a s x<VAR>n : ℕ<GOAL>DifferentiableWithinAt 𝕜 (fun x => a x ^ n) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableAt 𝕜 a x<VAR>n : ℕ<GOAL>DifferentiableAt 𝕜 (fun x => a x ^ n) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableOn 𝕜 a s<VAR>n : ℕ<GOAL>DifferentiableOn 𝕜 (fun x => a x ^ n) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : Differentiable 𝕜 a<VAR>n : ℕ<GOAL>Differentiable 𝕜 fun x => a x ^ n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>ha : DifferentiableWithinAt 𝕜 a s x<VAR>hb : DifferentiableWithinAt 𝕜 b s x<GOAL>fderivWithin 𝕜 (fun y => a y * b y) s x = a x • fderivWithin 𝕜 b s x + (fderivWithin 𝕜 a s x).smulRight (b x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c d : E → 𝔸'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hd : DifferentiableWithinAt 𝕜 d s x<GOAL>fderivWithin 𝕜 (fun y => c y * d y) s x = c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a b : E → 𝔸<VAR>ha : DifferentiableAt 𝕜 a x<VAR>hb : DifferentiableAt 𝕜 b x<GOAL>fderiv 𝕜 (fun y => a y * b y) x = a x • fderiv 𝕜 b x + (fderiv 𝕜 a x).smulRight (b x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c d : E → 𝔸'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hd : DifferentiableAt 𝕜 d x<GOAL>fderiv 𝕜 (fun y => c y * d y) x = c x • fderiv 𝕜 d x + d x • fderiv 𝕜 c x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>a' : E →L[𝕜] 𝔸<VAR>ha : HasStrictFDerivAt a a' x<VAR>b : 𝔸<GOAL>HasStrictFDerivAt (fun y => a y * b) (a'.smulRight b) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c : E → 𝔸'<VAR>c' : E →L[𝕜] 𝔸'<VAR>hc : HasStrictFDerivAt c c' x<VAR>d : 𝔸'<GOAL>HasStrictFDerivAt (fun y => c y * d) (d • c') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>a' : E →L[𝕜] 𝔸<VAR>ha : HasFDerivWithinAt a a' s x<VAR>b : 𝔸<GOAL>HasFDerivWithinAt (fun y => a y * b) (a'.smulRight b) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c : E → 𝔸'<VAR>c' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivWithinAt c c' s x<VAR>d : 𝔸'<GOAL>HasFDerivWithinAt (fun y => c y * d) (d • c') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>a' : E →L[𝕜] 𝔸<VAR>ha : HasFDerivAt a a' x<VAR>b : 𝔸<GOAL>HasFDerivAt (fun y => a y * b) (a'.smulRight b) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c : E → 𝔸'<VAR>c' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivAt c c' x<VAR>d : 𝔸'<GOAL>HasFDerivAt (fun y => c y * d) (d • c') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableWithinAt 𝕜 a s x<VAR>b : 𝔸<GOAL>DifferentiableWithinAt 𝕜 (fun y => a y * b) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableAt 𝕜 a x<VAR>b : 𝔸<GOAL>DifferentiableAt 𝕜 (fun y => a y * b) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableOn 𝕜 a s<VAR>b : 𝔸<GOAL>DifferentiableOn 𝕜 (fun y => a y * b) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : Differentiable 𝕜 a<VAR>b : 𝔸<GOAL>Differentiable 𝕜 fun y => a y * b
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>ha : DifferentiableWithinAt 𝕜 a s x<VAR>b : 𝔸<GOAL>fderivWithin 𝕜 (fun y => a y * b) s x = (fderivWithin 𝕜 a s x).smulRight b
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c : E → 𝔸'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>d : 𝔸'<GOAL>fderivWithin 𝕜 (fun y => c y * d) s x = d • fderivWithin 𝕜 c s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableAt 𝕜 a x<VAR>b : 𝔸<GOAL>fderiv 𝕜 (fun y => a y * b) x = (fderiv 𝕜 a x).smulRight b
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸' : Type u_7<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>c : E → 𝔸'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>d : 𝔸'<GOAL>fderiv 𝕜 (fun y => c y * d) x = d • fderiv 𝕜 c x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>a' : E →L[𝕜] 𝔸<VAR>ha : HasStrictFDerivAt a a' x<VAR>b : 𝔸<GOAL>HasStrictFDerivAt (fun y => b * a y) (b • a') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>a' : E →L[𝕜] 𝔸<VAR>ha : HasFDerivWithinAt a a' s x<VAR>b : 𝔸<GOAL>HasFDerivWithinAt (fun y => b * a y) (b • a') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>a' : E →L[𝕜] 𝔸<VAR>ha : HasFDerivAt a a' x<VAR>b : 𝔸<GOAL>HasFDerivAt (fun y => b * a y) (b • a') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableWithinAt 𝕜 a s x<VAR>b : 𝔸<GOAL>DifferentiableWithinAt 𝕜 (fun y => b * a y) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableAt 𝕜 a x<VAR>b : 𝔸<GOAL>DifferentiableAt 𝕜 (fun y => b * a y) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableOn 𝕜 a s<VAR>b : 𝔸<GOAL>DifferentiableOn 𝕜 (fun y => b * a y) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : Differentiable 𝕜 a<VAR>b : 𝔸<GOAL>Differentiable 𝕜 fun y => b * a y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>ha : DifferentiableWithinAt 𝕜 a s x<VAR>b : 𝔸<GOAL>fderivWithin 𝕜 (fun y => b * a y) s x = b • fderivWithin 𝕜 a s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝔸 : Type u_6<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>a : E → 𝔸<VAR>ha : DifferentiableAt 𝕜 a x<VAR>b : 𝔸<GOAL>fderiv 𝕜 (fun y => b * a y) x = b • fderiv 𝕜 a x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>Fintype ι<VAR>l : List ι<VAR>x : ι → 𝔸<GOAL>HasStrictFDerivAt (fun x => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (ContinuousLinearMap.proj (l.get i)).smulRight (List.map x (List.drop (↑i).succ l)).prod) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝔸 : Type u_7<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>n : ℕ<VAR>x : Fin n → 𝔸<GOAL>HasStrictFDerivAt (fun x => (List.map x (List.finRange n)).prod) (∑ i : Fin n, (List.map x (List.take (↑i) (List.finRange n))).prod • (ContinuousLinearMap.proj i).smulRight (List.map x (List.drop (↑i).succ (List.finRange n))).prod) x