ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>Fintype ι<VAR>F' : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)<GOAL>HasFTaylorSeriesUpToOn n (fun x i => φ i x) (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔ ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>Fintype ι<VAR>F' : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)<GOAL>HasFTaylorSeriesUpToOn n Φ P' s ↔ ∀ (i : ι), HasFTaylorSeriesUpToOn n (fun x => Φ x i) (fun x m => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>Fintype ι<VAR>F' : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<GOAL>ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>Fintype ι<VAR>F' : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<GOAL>ContDiffOn 𝕜 n Φ s ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => Φ x i) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>Fintype ι<VAR>F' : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<GOAL>ContDiffAt 𝕜 n Φ x ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x => Φ x i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>Fintype ι<VAR>F' : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<GOAL>ContDiff 𝕜 n Φ ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => Φ x i
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_3<VAR>Fintype ι<VAR>F' : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>DecidableEq ι<VAR>k : ℕ∞<VAR>x : (i : ι) → F' i<VAR>i : ι<GOAL>ContDiff 𝕜 k (Function.update x i)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_3<VAR>Fintype ι<VAR>F' : ι → Type u_5<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>DecidableEq ι<VAR>k : ℕ∞<VAR>i : ι<GOAL>ContDiff 𝕜 k (Pi.single i)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>Fintype ι<VAR>i : ι<GOAL>ContDiff 𝕜 n fun f => f i
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>Fintype ι<VAR>Fintype ι'<VAR>i : ι<VAR>j : ι'<GOAL>ContDiff 𝕜 n fun f => f i j
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>q : E → FormalMultilinearSeries 𝕜 E F<VAR>g : E → F<VAR>hf : HasFTaylorSeriesUpToOn n f p s<VAR>hg : HasFTaylorSeriesUpToOn n g q s<GOAL>HasFTaylorSeriesUpToOn n (f + g) (p + q) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n fun p => p.1 + p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>s : Set E<VAR>f g : E → F<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x + g x) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>f g : E → F<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<GOAL>ContDiffAt 𝕜 n (fun x => f x + g x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f g : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n fun x => f x + g x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>s : Set E<VAR>f g : E → F<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hg : ContDiffOn 𝕜 n g s<GOAL>ContDiffOn 𝕜 n (fun x => f x + g x) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>i : ℕ<VAR>f g : E → F<VAR>hf : ContDiffOn 𝕜 (↑i) f s<VAR>hg : ContDiffOn 𝕜 (↑i) g s<VAR>hu : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>i : ℕ<VAR>f g : E → F<VAR>hf : ContDiffOn 𝕜 (↑i) f s<VAR>hg : ContDiffOn 𝕜 (↑i) g s<VAR>hu : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedFDerivWithin 𝕜 i (fun x => f x + g x) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>i : ℕ<VAR>f g : E → F<VAR>hf : ContDiff 𝕜 (↑i) f<VAR>hg : ContDiff 𝕜 (↑i) g<GOAL>iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>i : ℕ<VAR>f g : E → F<VAR>hf : ContDiff 𝕜 (↑i) f<VAR>hg : ContDiff 𝕜 (↑i) g<GOAL>iteratedFDeriv 𝕜 i (fun x => f x + g x) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n fun p => -p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : E → F<VAR>hf : ContDiffWithinAt 𝕜 n f s x<GOAL>ContDiffWithinAt 𝕜 n (fun x => -f x) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>f : E → F<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (fun x => -f x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E → F<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => -f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : E → F<VAR>hf : ContDiffOn 𝕜 n f s<GOAL>ContDiffOn 𝕜 n (fun x => -f x) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>i : ℕ<VAR>f : E → F<VAR>hu : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>i : ℕ<VAR>f : E → F<GOAL>iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>s : Set E<VAR>f g : E → F<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>f g : E → F<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<GOAL>ContDiffAt 𝕜 n (fun x => f x - g x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>s : Set E<VAR>f g : E → F<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hg : ContDiffOn 𝕜 n g s<GOAL>ContDiffOn 𝕜 n (fun x => f x - g x) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f g : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n fun x => f x - g x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>s : Finset ι<VAR>t : Set E<VAR>x : E<VAR>h : ∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun x => f i x) t x<GOAL>ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>s : Finset ι<VAR>x : E<VAR>h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun x => f i x) x<GOAL>ContDiffAt 𝕜 n (fun x => ∑ i ∈ s, f i x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>s : Finset ι<VAR>t : Set E<VAR>h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun x => f i x) t<GOAL>ContDiffOn 𝕜 n (fun x => ∑ i ∈ s, f i x) t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, ContDiff 𝕜 n fun x => f i x<GOAL>ContDiff 𝕜 n fun x => ∑ i ∈ s, f i x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>u : Finset ι<VAR>i : ℕ<VAR>x : E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>h : ∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s<GOAL>iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_3<VAR>f : ι → E → F<VAR>u : Finset ι<VAR>i : ℕ<VAR>h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j)<GOAL>(iteratedFDeriv 𝕜 i fun x => ∑ j ∈ u, f j x) = ∑ j ∈ u, iteratedFDeriv 𝕜 i (f j)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<GOAL>ContDiff 𝕜 n fun p => p.1 * p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>s : Set E<VAR>f g : E → 𝔸<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x * g x) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f g : E → 𝔸<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<GOAL>ContDiffAt 𝕜 n (fun x => f x * g x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f g : E → 𝔸<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hg : ContDiffOn 𝕜 n g s<GOAL>ContDiffOn 𝕜 n (fun x => f x * g x) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f g : E → 𝔸<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n fun x => f x * g x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>n : ℕ∞<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x<GOAL>ContDiffWithinAt 𝕜 n (∏ i ∈ t, f i) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>n : ℕ∞<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x<GOAL>ContDiffWithinAt 𝕜 n (fun y => ∏ i ∈ t, f i y) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>n : ℕ∞<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x<GOAL>ContDiffAt 𝕜 n (∏ i ∈ t, f i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>n : ℕ∞<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x<GOAL>ContDiffAt 𝕜 n (fun y => ∏ i ∈ t, f i y) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>n : ℕ∞<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s<GOAL>ContDiffOn 𝕜 n (∏ i ∈ t, f i) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>n : ℕ∞<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s<GOAL>ContDiffOn 𝕜 n (fun y => ∏ i ∈ t, f i y) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiff 𝕜 n (f i)<GOAL>ContDiff 𝕜 n (∏ i ∈ t, f i)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>𝔸' : Type u_4<VAR>ι : Type u_5<VAR>NormedCommRing 𝔸'<VAR>NormedAlgebra 𝕜 𝔸'<VAR>t : Finset ι<VAR>f : ι → E → 𝔸'<VAR>h : ∀ i ∈ t, ContDiff 𝕜 n (f i)<GOAL>ContDiff 𝕜 n fun y => ∏ i ∈ t, f i y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : E → 𝔸<VAR>hf : ContDiff 𝕜 n f<VAR>m : ℕ<GOAL>ContDiff 𝕜 n fun x => f x ^ m
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : E → 𝔸<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>m : ℕ<GOAL>ContDiffWithinAt 𝕜 n (fun y => f y ^ m) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : E → 𝔸<VAR>hf : ContDiffAt 𝕜 n f x<VAR>m : ℕ<GOAL>ContDiffAt 𝕜 n (fun y => f y ^ m) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>n : ℕ∞<VAR>𝔸 : Type u_3<VAR>NormedRing 𝔸<VAR>NormedAlgebra 𝕜 𝔸<VAR>f : E → 𝔸<VAR>hf : ContDiffOn 𝕜 n f s<VAR>m : ℕ<GOAL>ContDiffOn 𝕜 n (fun y => f y ^ m) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>c : 𝕜'<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x / c) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>𝕜' : Type u_6<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕜 n f x<VAR>c : 𝕜'<GOAL>ContDiffAt 𝕜 n (fun x => f x / c) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>𝕜' : Type u_6<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiffOn 𝕜 n f s<VAR>c : 𝕜'<GOAL>ContDiffOn 𝕜 n (fun x => f x / c) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_6<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>c : 𝕜'<GOAL>ContDiff 𝕜 n fun x => f x / c
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<GOAL>ContDiff 𝕜 n fun p => p.1 • p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : E → 𝕜<VAR>g : E → F<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x • g x) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : E<VAR>n : ℕ∞<VAR>f : E → 𝕜<VAR>g : E → F<VAR>hf : ContDiffAt 𝕜 n f x<VAR>hg : ContDiffAt 𝕜 n g x<GOAL>ContDiffAt 𝕜 n (fun x => f x • g x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E → 𝕜<VAR>g : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n fun x => f x • g x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>s : Set E<VAR>f : E → 𝕜<VAR>g : E → F<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hg : ContDiffOn 𝕜 n g s<GOAL>ContDiffOn 𝕜 n (fun x => f x • g x) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>c : R<GOAL>ContDiff 𝕜 n fun p => c • p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>c : R<VAR>hf : ContDiffWithinAt 𝕜 n f s x<GOAL>ContDiffWithinAt 𝕜 n (fun y => c • f y) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>f : E → F<VAR>x : E<VAR>c : R<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (fun y => c • f y) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>f : E → F<VAR>c : R<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun y => c • f y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>s : Set E<VAR>f : E → F<VAR>c : R<VAR>hf : ContDiffOn 𝕜 n f s<GOAL>ContDiffOn 𝕜 n (fun y => c • f y) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>i : ℕ<VAR>a : R<VAR>hf : ContDiffOn 𝕜 (↑i) f s<VAR>hu : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<GOAL>iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>i : ℕ<VAR>a : R<VAR>x : E<VAR>hf : ContDiff 𝕜 (↑i) f<GOAL>iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>R : Type u_3<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>i : ℕ<VAR>a : R<VAR>x : E<VAR>hf : ContDiff 𝕜 (↑i) f<GOAL>iteratedFDeriv 𝕜 i (fun x => a • f x) x = a • iteratedFDeriv 𝕜 i f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>s : Set E<VAR>t : Set E'<VAR>f : E → F<VAR>g : E' → F'<VAR>p : E × E'<VAR>hf : ContDiffWithinAt 𝕜 n f s p.1<VAR>hg : ContDiffWithinAt 𝕜 n g t p.2<GOAL>ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>s : Set E<VAR>t : Set E'<VAR>f : E → F<VAR>g : E' → F'<VAR>x : E<VAR>y : E'<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g t y<GOAL>ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y)