ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>n : ℕ∞<VAR>Eu : Type u<VAR>NormedAddCommGroup Eu<VAR>NormedSpace 𝕜 Eu<VAR>Fu : Type u<VAR>NormedAddCommGroup Fu<VAR>NormedSpace 𝕜 Fu<VAR>Gu : Type u<VAR>NormedAddCommGroup Gu<VAR>NormedSpace 𝕜 Gu<VAR>s : Set Eu<VAR>t : Set Fu<VAR>g : Fu → Gu<VAR>f : Eu → Fu<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<GOAL>ContDiffOn 𝕜 n (g ∘ f) 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<VAR>st : s ⊆ f ⁻¹' t<GOAL>ContDiffOn 𝕜 n (g ∘ f) 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiffOn 𝕜 n g t<VAR>hf : ContDiffOn 𝕜 n f s<GOAL>ContDiffOn 𝕜 n (g ∘ f) (s ∩ f ⁻¹' 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>s : Set E<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiff 𝕜 n g<VAR>hf : ContDiffOn 𝕜 n f s<GOAL>ContDiffOn 𝕜 n (g ∘ f) 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>g : F → G<VAR>f : E → F<VAR>hg : ContDiff 𝕜 n g<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n (g ∘ f)
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>st : s ⊆ f ⁻¹' t<GOAL>ContDiffWithinAt 𝕜 n (g ∘ 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hs : t ∈ 𝓝[f '' s] f x<GOAL>ContDiffWithinAt 𝕜 n (g ∘ 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<GOAL>ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F<VAR>g : F → G<VAR>n : ℕ∞<VAR>x : E<VAR>hg : ContDiffAt 𝕜 n g (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<GOAL>ContDiffWithinAt 𝕜 n (g ∘ 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>g : F → G<VAR>n : ℕ∞<VAR>x : E<VAR>hg : ContDiffAt 𝕜 n g (f x)<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (g ∘ 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>t : Set E<VAR>x : E<VAR>n : ℕ∞<VAR>g : F → G<VAR>f : E → F<VAR>h : ContDiff 𝕜 n g<VAR>hf : ContDiffWithinAt 𝕜 n f t x<GOAL>ContDiffWithinAt 𝕜 n (g ∘ f) 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiff 𝕜 n g<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (g ∘ 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 : ℕ∞<GOAL>ContDiff 𝕜 n Prod.fst
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F × G<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => (f x).1
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → G<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => f x.1
<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 × F)<GOAL>ContDiffOn 𝕜 n Prod.fst 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F × G<VAR>s : Set E<VAR>hf : ContDiffOn 𝕜 n f s<GOAL>ContDiffOn 𝕜 n (fun x => (f x).1) 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>p : E × F<GOAL>ContDiffAt 𝕜 n Prod.fst 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F × G<VAR>x : E<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (fun x => (f x).1) 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → G<VAR>x : E<VAR>y : F<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (fun x => f x.1) (x, 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → G<VAR>x : E × F<VAR>hf : ContDiffAt 𝕜 n f x.1<GOAL>ContDiffAt 𝕜 n (fun x => f x.1) 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 × F)<VAR>p : E × F<GOAL>ContDiffWithinAt 𝕜 n Prod.fst s 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 : ℕ∞<GOAL>ContDiff 𝕜 n Prod.snd
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F × G<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => (f x).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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : F → G<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => f x.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>n : ℕ∞<VAR>s : Set (E × F)<GOAL>ContDiffOn 𝕜 n Prod.snd 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F × G<VAR>s : Set E<VAR>hf : ContDiffOn 𝕜 n f s<GOAL>ContDiffOn 𝕜 n (fun x => (f x).2) 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>p : E × F<GOAL>ContDiffAt 𝕜 n Prod.snd 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : E → F × G<VAR>x : E<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (fun x => (f x).2) 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : F → G<VAR>x : E<VAR>y : F<VAR>hf : ContDiffAt 𝕜 n f y<GOAL>ContDiffAt 𝕜 n (fun x => f x.2) (x, 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>f : F → G<VAR>x : E × F<VAR>hf : ContDiffAt 𝕜 n f x.2<GOAL>ContDiffAt 𝕜 n (fun x => f x.2) 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 × F)<VAR>p : E × F<GOAL>ContDiffWithinAt 𝕜 n Prod.snd s p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>E₁ : Type u_3<VAR>E₂ : Type u_4<VAR>NormedAddCommGroup E₁<VAR>NormedAddCommGroup E₂<VAR>NormedSpace 𝕜 E₁<VAR>NormedSpace 𝕜 E₂<VAR>g : E₁ × E₂ → G<VAR>f₁ : F → E₁<VAR>f₂ : F → E₂<VAR>hg : ContDiff 𝕜 n g<VAR>hf₁ : ContDiff 𝕜 n f₁<VAR>hf₂ : ContDiff 𝕜 n f₂<GOAL>ContDiff 𝕜 n fun x => g (f₁ x, f₂ x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>E₁ : Type u_3<VAR>E₂ : Type u_4<VAR>E₃ : Type u_5<VAR>NormedAddCommGroup E₁<VAR>NormedAddCommGroup E₂<VAR>NormedAddCommGroup E₃<VAR>NormedSpace 𝕜 E₁<VAR>NormedSpace 𝕜 E₂<VAR>NormedSpace 𝕜 E₃<VAR>g : E₁ × E₂ × E₃ → G<VAR>f₁ : F → E₁<VAR>f₂ : F → E₂<VAR>f₃ : F → E₃<VAR>hg : ContDiff 𝕜 n g<VAR>hf₁ : ContDiff 𝕜 n f₁<VAR>hf₂ : ContDiff 𝕜 n f₂<VAR>hf₃ : ContDiff 𝕜 n f₃<GOAL>ContDiff 𝕜 n fun x => g (f₁ x, f₂ x, f₃ x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>E₁ : Type u_3<VAR>E₂ : Type u_4<VAR>NormedAddCommGroup E₁<VAR>NormedAddCommGroup E₂<VAR>NormedSpace 𝕜 E₁<VAR>NormedSpace 𝕜 E₂<VAR>g : E₁ × E₂ → G<VAR>f₁ : F → E₁<VAR>f₂ : F → E₂<VAR>s : Set F<VAR>hg : ContDiff 𝕜 n g<VAR>hf₁ : ContDiffOn 𝕜 n f₁ s<VAR>hf₂ : ContDiffOn 𝕜 n f₂ s<GOAL>ContDiffOn 𝕜 n (fun x => g (f₁ x, f₂ x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>E₁ : Type u_3<VAR>E₂ : Type u_4<VAR>E₃ : Type u_5<VAR>NormedAddCommGroup E₁<VAR>NormedAddCommGroup E₂<VAR>NormedAddCommGroup E₃<VAR>NormedSpace 𝕜 E₁<VAR>NormedSpace 𝕜 E₂<VAR>NormedSpace 𝕜 E₃<VAR>g : E₁ × E₂ × E₃ → G<VAR>f₁ : F → E₁<VAR>f₂ : F → E₂<VAR>f₃ : F → E₃<VAR>s : Set F<VAR>hg : ContDiff 𝕜 n g<VAR>hf₁ : ContDiffOn 𝕜 n f₁ s<VAR>hf₂ : ContDiffOn 𝕜 n f₂ s<VAR>hf₃ : ContDiffOn 𝕜 n f₃ s<GOAL>ContDiffOn 𝕜 n (fun x => g (f₁ x, f₂ 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedSpace 𝕜 X<VAR>n : ℕ∞<VAR>g : X → F →L[𝕜] G<VAR>f : X → E →L[𝕜] F<VAR>hg : ContDiff 𝕜 n g<VAR>hf : ContDiff 𝕜 n f<GOAL>ContDiff 𝕜 n fun x => (g x).comp (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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>NormedAddCommGroup X<VAR>NormedSpace 𝕜 X<VAR>n : ℕ∞<VAR>g : X → F →L[𝕜] G<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<VAR>hg : ContDiffOn 𝕜 n g s<VAR>hf : ContDiffOn 𝕜 n f s<GOAL>ContDiffOn 𝕜 n (fun x => (g x).comp (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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F →L[𝕜] G<VAR>g : E → F<VAR>n : ℕ∞<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F →L[𝕜] G<VAR>g : E → F<VAR>n : ℕ∞<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F →L[𝕜] 𝕜<VAR>g : E → G<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n fun x => (f x).smulRight (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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>n : ℕ∞<VAR>c : E → F →L[𝕜] G<VAR>hc : ContDiffOn 𝕜 n c s<VAR>i : ℕ<VAR>hi : ↑i ≤ n<VAR>x : E<VAR>hx : x ∈ s<VAR>u : F<VAR>m : Fin i → E<GOAL>(iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>n : ℕ∞<VAR>c : E → F →L[𝕜] G<VAR>hc : ContDiff 𝕜 n c<VAR>i : ℕ<VAR>hi : ↑i ≤ n<VAR>x : E<VAR>u : F<VAR>m : Fin i → E<GOAL>(iteratedFDeriv 𝕜 i (fun y => (c y) u) x) m = ((iteratedFDeriv 𝕜 i c x) m) u
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<GOAL>ContDiff 𝕜 ⊤ ⇑(Equiv.prodAssoc E F G)
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<GOAL>ContDiff 𝕜 ⊤ ⇑(Equiv.prodAssoc E F G).symm
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ<VAR>x₀ : E<VAR>hf : ContDiffWithinAt 𝕜 (↑n + 1) (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 (↑n) g s x₀<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<GOAL>∃ v ∈ 𝓝[insert x₀ s] x₀, v ⊆ insert x₀ s ∧ ∃ f', (∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x₀ : E<VAR>m : ℕ∞<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)<VAR>hmn : m + 1 ≤ n<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<GOAL>ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x₀ : E<VAR>m : ℕ∞<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)<VAR>hmn : m + 1 ≤ n<VAR>hst : s ⊆ g ⁻¹' t<GOAL>ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x₀ : E<VAR>m : ℕ∞<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hmn : m + 1 ≤ n<VAR>hx₀ : x₀ ∈ s<VAR>hst : s ⊆ g ⁻¹' t<GOAL>ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>x₀ : E<VAR>m : ℕ∞<VAR>f : E → F → G<VAR>g k : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>hk : ContDiffWithinAt 𝕜 m k s x₀<VAR>ht : UniqueDiffOn 𝕜 t<VAR>hmn : m + 1 ≤ n<VAR>hx₀ : x₀ ∈ s<VAR>hst : s ⊆ g ⁻¹' t<GOAL>ContDiffWithinAt 𝕜 m (fun x => (fderivWithin 𝕜 (f x) t (g x)) (k 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>s : Set E<VAR>f : E → F<VAR>x₀ : E<VAR>m n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n f s x₀<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hmn : m + 1 ≤ n<VAR>hx₀s : x₀ ∈ s<GOAL>ContDiffWithinAt 𝕜 m (fderivWithin 𝕜 f s) 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>f : E → F<VAR>x₀ : E<VAR>m n : ℕ∞<VAR>i : ℕ<VAR>hf : ContDiffWithinAt 𝕜 n f s x₀<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hmn : m + ↑i ≤ n<VAR>hx₀s : x₀ ∈ s<GOAL>ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 i f s) 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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>x₀ : E<VAR>m : ℕ∞<VAR>f : E → F → G<VAR>g : E → F<VAR>n : ℕ∞<VAR>hf : ContDiffAt 𝕜 n (Function.uncurry f) (x₀, g x₀)<VAR>hg : ContDiffAt 𝕜 m g x₀<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (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>f : E → F<VAR>x₀ : E<VAR>m n : ℕ∞<VAR>hf : ContDiffAt 𝕜 n f x₀<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffAt 𝕜 m (fderiv 𝕜 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>x₀ : E<VAR>m n : ℕ∞<VAR>i : ℕ<VAR>hf : ContDiffAt 𝕜 n f x₀<VAR>hmn : m + ↑i ≤ n<GOAL>ContDiffAt 𝕜 m (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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F → G<VAR>g : E → F<VAR>n m : ℕ∞<VAR>hf : ContDiff 𝕜 m (Function.uncurry f)<VAR>hg : ContDiff 𝕜 n g<VAR>hnm : n + 1 ≤ m<GOAL>ContDiff 𝕜 n fun x => fderiv 𝕜 (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>f : E → F<VAR>m n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>hmn : m + 1 ≤ n<GOAL>ContDiff 𝕜 m (fderiv 𝕜 f)
<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>m n : ℕ∞<VAR>i : ℕ<VAR>hf : ContDiff 𝕜 n f<VAR>hmn : m + ↑i ≤ n<GOAL>ContDiff 𝕜 m (iteratedFDeriv 𝕜 i f)
<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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F → G<VAR>g : E → F<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n (Function.uncurry f)<VAR>hg : Continuous g<VAR>hn : 1 ≤ n<GOAL>Continuous fun x => fderiv 𝕜 (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>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F → G<VAR>g k : E → F<VAR>n m : ℕ∞<VAR>hf : ContDiff 𝕜 m (Function.uncurry f)<VAR>hg : ContDiff 𝕜 n g<VAR>hk : ContDiff 𝕜 n k<VAR>hnm : n + 1 ≤ m<GOAL>ContDiff 𝕜 n fun x => (fderiv 𝕜 (f x) (g x)) (k 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>m n : ℕ∞<VAR>s : Set E<VAR>f : E → F<VAR>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hmn : m + 1 ≤ n<GOAL>ContDiffOn 𝕜 m (fun p => (fderivWithin 𝕜 f s p.1) p.2) (s ×ˢ Set.univ)
<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>hf : ContDiffOn 𝕜 n f s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hn : 1 ≤ n<GOAL>ContinuousOn (fun p => (fderivWithin 𝕜 f s p.1) p.2) (s ×ˢ Set.univ)
<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>m n : ℕ∞<VAR>f : E → F<VAR>hf : ContDiff 𝕜 n f<VAR>hmn : m + 1 ≤ n<GOAL>ContDiff 𝕜 m fun p => (fderiv 𝕜 f p.1) p.2