ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c : 𝕜 → 𝔸<VAR>c' : 𝔸<VAR>hc : HasDerivAt c c' x<VAR>d : 𝔸<GOAL>HasDerivAt (fun y => c y * d) (c' * d) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>c : 𝕜<GOAL>HasDerivAt (fun x => x * c) c x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c : 𝕜 → 𝔸<VAR>c' : 𝔸<VAR>hc : HasStrictDerivAt c c' x<VAR>d : 𝔸<GOAL>HasStrictDerivAt (fun y => c y * d) (c' * d) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c : 𝕜 → 𝔸<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>d : 𝔸<GOAL>derivWithin (fun y => c y * d) s x = derivWithin c s x * d
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>c : 𝕜 → 𝔸<VAR>hc : DifferentiableAt 𝕜 c x<VAR>d : 𝔸<GOAL>deriv (fun y => c y * d) x = deriv c x * d
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>u : 𝕜 → 𝕜'<VAR>v : 𝕜'<GOAL>deriv (fun y => u y * v) x = deriv u x * v
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>u : 𝕜 → 𝕜'<VAR>v : 𝕜'<GOAL>(deriv fun x => u x * v) = fun x => deriv u x * v
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>d : 𝕜 → 𝔸<VAR>d' : 𝔸<VAR>c : 𝔸<VAR>hd : HasDerivWithinAt d d' s x<GOAL>HasDerivWithinAt (fun y => c * d y) (c * d') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>d : 𝕜 → 𝔸<VAR>d' : 𝔸<VAR>c : 𝔸<VAR>hd : HasDerivAt d d' x<GOAL>HasDerivAt (fun y => c * d y) (c * d') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>d : 𝕜 → 𝔸<VAR>d' : 𝔸<VAR>c : 𝔸<VAR>hd : HasStrictDerivAt d d' x<GOAL>HasStrictDerivAt (fun y => c * d y) (c * d') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>d : 𝕜 → 𝔸<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : 𝔸<VAR>hd : DifferentiableWithinAt 𝕜 d s x<GOAL>derivWithin (fun y => c * d y) s x = c * derivWithin d s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>d : 𝕜 → 𝔸<VAR>c : 𝔸<VAR>hd : DifferentiableAt 𝕜 d x<GOAL>deriv (fun y => c * d y) x = c * deriv d x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>v : 𝕜 → 𝕜'<VAR>u : 𝕜'<GOAL>deriv (fun y => u * v y) x = u * deriv v x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>v : 𝕜 → 𝕜'<VAR>u : 𝕜'<GOAL>(deriv fun x => u * v x) = fun x => u * deriv v x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>f' : ι → 𝔸'<VAR>hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x<GOAL>HasDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>f' : ι → 𝔸'<VAR>hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x<GOAL>HasDerivWithinAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>f' : ι → 𝔸'<VAR>hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x<GOAL>HasStrictDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>hf : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x<GOAL>deriv (fun x => ∏ i ∈ u, f i x) x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • deriv (f i) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>ι : Type u_2<VAR>DecidableEq ι<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x<GOAL>derivWithin (fun x => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>ι : Type u_2<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x<GOAL>DifferentiableAt 𝕜 (fun x => ∏ i ∈ u, f i x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>ι : Type u_2<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x<GOAL>DifferentiableWithinAt 𝕜 (fun x => ∏ i ∈ u, f i x) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>ι : Type u_2<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>hd : ∀ i ∈ u, DifferentiableOn 𝕜 (f i) s<GOAL>DifferentiableOn 𝕜 (fun x => ∏ i ∈ u, f i x) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_2<VAR>𝔸' : Type u_3<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → 𝕜 → 𝔸'<VAR>hd : ∀ i ∈ u, Differentiable 𝕜 (f i)<GOAL>Differentiable 𝕜 fun x => ∏ i ∈ u, f i x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>d : 𝕜'<GOAL>HasDerivAt (fun x => c x / d) (c' / d) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>d : 𝕜'<GOAL>HasDerivWithinAt (fun x => c x / d) (c' / d) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>d : 𝕜'<GOAL>HasStrictDerivAt (fun x => c x / d) (c' / d) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>d : 𝕜'<GOAL>DifferentiableWithinAt 𝕜 (fun x => c x / d) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>d : 𝕜'<GOAL>DifferentiableAt 𝕜 (fun x => c x / d) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>hc : DifferentiableOn 𝕜 c s<VAR>d : 𝕜'<GOAL>DifferentiableOn 𝕜 (fun x => c x / d) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>hc : Differentiable 𝕜 c<VAR>d : 𝕜'<GOAL>Differentiable 𝕜 fun x => c x / d
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>d : 𝕜'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => c x / d) s x = derivWithin c s x / d
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c : 𝕜 → 𝕜'<VAR>d : 𝕜'<GOAL>deriv (fun x => c x / d) x = deriv c x / d
<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>x : 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<GOAL>HasStrictDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') 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>x : 𝕜<VAR>s : Set 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>hc : HasDerivWithinAt c c' s x<VAR>hd : HasDerivWithinAt d d' s x<GOAL>HasDerivWithinAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') 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>x : 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>d' : E →L[𝕜] F<VAR>hc : HasDerivAt c c' x<VAR>hd : HasDerivAt d d' x<GOAL>HasDerivAt (fun y => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') 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>x : 𝕜<VAR>s : Set 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hd : DifferentiableWithinAt 𝕜 d s x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun y => (c y).comp (d y)) s x = (derivWithin c s x).comp (d x) + (c x).comp (derivWithin d 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>x : 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>d : 𝕜 → E →L[𝕜] F<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hd : DifferentiableAt 𝕜 d x<GOAL>deriv (fun y => (c y).comp (d y)) x = (deriv c x).comp (d x) + (c x).comp (deriv d x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasStrictDerivAt c c' x<VAR>hu : HasStrictDerivAt u u' x<GOAL>HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasDerivWithinAt c c' s x<VAR>hu : HasDerivWithinAt u u' s x<GOAL>HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>c' : F →L[𝕜] G<VAR>u : 𝕜 → F<VAR>u' : F<VAR>hc : HasDerivAt c c' x<VAR>hu : HasDerivAt u u' x<GOAL>HasDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>u : 𝕜 → F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hu : DifferentiableWithinAt 𝕜 u s x<GOAL>derivWithin (fun y => (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : 𝕜<VAR>G : Type u_2<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>c : 𝕜 → F →L[𝕜] G<VAR>u : 𝕜 → F<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hu : DifferentiableAt 𝕜 u x<GOAL>deriv (fun y => (c y) (u y)) x = (deriv c x) (u x) + (c x) (deriv u x)
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ x ∈ Metric.ball x₀ ε, MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>hF_int : MeasureTheory.Integrable (F x₀) μ<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ<VAR>h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F x a - F x₀ a‖ ≤ bound a * ‖x - x₀‖<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀<GOAL>MeasureTheory.Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>hF_int : MeasureTheory.Integrable (F x₀) μ<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ<VAR>h_lip : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (Metric.ball x₀ ε)<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x => F x a) (F' a) x₀<GOAL>MeasureTheory.Integrable F' μ ∧ HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_4<VAR>NormedAddCommGroup H<VAR>x₀ : H<VAR>ε : ℝ<VAR>NormedSpace ℝ H<VAR>μ : MeasureTheory.Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (Metric.ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x => F x t) (F' t) x₀<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>NormedAddCommGroup H<VAR>NormedSpace 𝕜 H<VAR>F : H → α → E<VAR>x₀ : H<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F' : H → α → H →L[𝕜] E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>hF_int : MeasureTheory.Integrable (F x₀) μ<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, HasFDerivAt (fun x => F x a) (F' x a) x<GOAL>HasFDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' x₀ a ∂μ) x₀
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_4<VAR>NormedAddCommGroup H<VAR>x₀ : H<VAR>ε : ℝ<VAR>NormedSpace ℝ H<VAR>μ : MeasureTheory.Measure ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[ℝ] E<VAR>a b : ℝ<VAR>bound : ℝ → ℝ<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ Metric.ball x₀ ε, ‖F' x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ∀ x ∈ Metric.ball x₀ ε, HasFDerivAt (fun x => F x t) (F' x t) x<GOAL>HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>F' : α → E<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>hF_int : MeasureTheory.Integrable (F x₀) μ<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable F' μ<VAR>h_lipsch : ∀ᵐ (a : α) ∂μ, LipschitzOnWith (Real.nnabs (bound a)) (fun x => F x a) (Metric.ball x₀ ε)<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x => F x a) (F' a) x₀<GOAL>MeasureTheory.Integrable F' μ ∧ HasDerivAt (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>𝕜 : Type u_2<VAR>RCLike 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedSpace 𝕜 E<VAR>bound : α → ℝ<VAR>ε : ℝ<VAR>F : 𝕜 → α → E<VAR>x₀ : 𝕜<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (F x) μ<VAR>hF_int : MeasureTheory.Integrable (F x₀) μ<VAR>F' : 𝕜 → α → E<VAR>hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) μ<VAR>h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, ‖F' x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ Metric.ball x₀ ε, HasDerivAt (fun x => F x a) (F' x a) x<GOAL>MeasureTheory.Integrable (F' x₀) μ ∧ HasDerivAt (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), F' x₀ a ∂μ) 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>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>c : ℝ≥0<VAR>hc : Subsingleton E ∨ 0 < c<GOAL>∃ s ∈ 𝓝 a, ApproximatesLinearOn f f' s c
<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>CompleteSpace E<VAR>CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>h : LinearMap.range f' = ⊤<GOAL>Filter.map f (𝓝 a) = 𝓝 (f a)
<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>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>∃ s, a ∈ s ∧ IsOpen s ∧ ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>↑(HasStrictFDerivAt.toPartialHomeomorph f hf) = 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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>a ∈ (HasStrictFDerivAt.toPartialHomeomorph f hf).source
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>f a ∈ (HasStrictFDerivAt.toPartialHomeomorph f hf).target
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>Filter.map f (𝓝 a) = 𝓝 (f a)
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>HasStrictFDerivAt.localInverse f f' a hf = ↑(HasStrictFDerivAt.toPartialHomeomorph f hf).symm
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>∀ᶠ (x : E) in 𝓝 a, HasStrictFDerivAt.localInverse f f' a hf (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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>HasStrictFDerivAt.localInverse f f' a hf (f a) = a
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>∀ᶠ (y : F) in 𝓝 (f a), f (HasStrictFDerivAt.localInverse f f' a hf y) = 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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>ContinuousAt (HasStrictFDerivAt.localInverse f f' a hf) (f a)
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>Filter.Tendsto (HasStrictFDerivAt.localInverse f f' a hf) (𝓝 (f a)) (𝓝 a)
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<VAR>g : F → E<VAR>hg : ∀ᶠ (x : E) in 𝓝 a, g (f x) = x<GOAL>∀ᶠ (y : F) in 𝓝 (f a), g y = HasStrictFDerivAt.localInverse f f' a hf 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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<GOAL>HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (↑f'.symm) (f a)
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E ≃L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f (↑f') a<VAR>g : F → E<VAR>hg : ∀ᶠ (x : E) in 𝓝 a, g (f x) = x<GOAL>HasStrictFDerivAt g (↑f'.symm) (f a)
<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>CompleteSpace E<VAR>f : E → F<VAR>f' : E → E ≃L[𝕜] F<VAR>hf : ∀ (x : E), HasStrictFDerivAt f (↑(f' x)) x<GOAL>IsOpenMap 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>b : E × F → G<VAR>h : IsBoundedBilinearMap 𝕜 b<VAR>p : E × F<GOAL>HasStrictFDerivAt b (h.deriv p) p