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>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>NormedAddCommGroup F₄<VAR>NormedSpace 𝕜 F₄<VAR>n : ℕ∞<VAR>f : M → F₁ ≃L[𝕜] F₂<VAR>g : M → F₃ ≃L[𝕜] F₄<VAR>x : M<VAR>hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x => ↑(f x).symm) x<VAR>hg : ContMDiffAt I 𝓘(𝕜, F₃ →L[𝕜] F₄) n (fun x => ↑(g x)) x<GOAL>ContMDiffAt I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) n (fun y => ↑((f y).arrowCongr (g y))) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>NormedAddCommGroup F₄<VAR>NormedSpace 𝕜 F₄<VAR>n : ℕ∞<VAR>f : M → F₁ ≃L[𝕜] F₂<VAR>g : M → F₃ ≃L[𝕜] F₄<VAR>s : Set M<VAR>hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₁) n (fun x => ↑(f x).symm) s<VAR>hg : ContMDiffOn I 𝓘(𝕜, F₃ →L[𝕜] F₄) n (fun x => ↑(g x)) s<GOAL>ContMDiffOn I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) n (fun y => ↑((f y).arrowCongr (g y))) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>NormedAddCommGroup F₄<VAR>NormedSpace 𝕜 F₄<VAR>n : ℕ∞<VAR>f : M → F₁ ≃L[𝕜] F₂<VAR>g : M → F₃ ≃L[𝕜] F₄<VAR>hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₁) n fun x => ↑(f x).symm<VAR>hg : ContMDiff I 𝓘(𝕜, F₃ →L[𝕜] F₄) n fun x => ↑(g x)<GOAL>ContMDiff I 𝓘(𝕜, (F₁ →L[𝕜] F₃) →L[𝕜] F₂ →L[𝕜] F₄) n fun y => ↑((f y).arrowCongr (g y))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>NormedAddCommGroup F₄<VAR>NormedSpace 𝕜 F₄<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₃<VAR>f : M → F₂ →L[𝕜] F₄<VAR>s : Set M<VAR>x : M<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s x<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (fun x => (g x).prodMap (f x)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>NormedAddCommGroup F₄<VAR>NormedSpace 𝕜 F₄<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₃<VAR>f : M → F₂ →L[𝕜] F₄<VAR>x : M<VAR>hg : ContMDiffAt I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g x<VAR>hf : ContMDiffAt I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f x<GOAL>ContMDiffAt I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (fun x => (g x).prodMap (f x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>NormedAddCommGroup F₄<VAR>NormedSpace 𝕜 F₄<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₃<VAR>f : M → F₂ →L[𝕜] F₄<VAR>s : Set M<VAR>hg : ContMDiffOn I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g s<VAR>hf : ContMDiffOn I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f s<GOAL>ContMDiffOn I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n (fun x => (g x).prodMap (f x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F₁ : Type u_14<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>NormedAddCommGroup F₃<VAR>NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>NormedAddCommGroup F₄<VAR>NormedSpace 𝕜 F₄<VAR>n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₃<VAR>f : M → F₂ →L[𝕜] F₄<VAR>hg : ContMDiff I 𝓘(𝕜, F₁ →L[𝕜] F₃) n g<VAR>hf : ContMDiff I 𝓘(𝕜, F₂ →L[𝕜] F₄) n f<GOAL>ContMDiff I 𝓘(𝕜, F₁ × F₂ →L[𝕜] F₃ × F₄) n fun x => (g x).prodMap (f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<GOAL>Smooth (𝓘(𝕜, 𝕜).prod 𝓘(𝕜, V)) 𝓘(𝕜, V) fun p => p.1 • p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : M → 𝕜<VAR>g : M → V<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f s x<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, V) n g s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, V) n (fun p => f p • g p) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>n : ℕ∞<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : M → 𝕜<VAR>g : M → V<VAR>hf : ContMDiffAt I 𝓘(𝕜, 𝕜) n f x<VAR>hg : ContMDiffAt I 𝓘(𝕜, V) n g x<GOAL>ContMDiffAt I 𝓘(𝕜, V) n (fun p => f p • g p) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>n : ℕ∞<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : M → 𝕜<VAR>g : M → V<VAR>hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f s<VAR>hg : ContMDiffOn I 𝓘(𝕜, V) n g s<GOAL>ContMDiffOn I 𝓘(𝕜, V) n (fun p => f p • g p) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>n : ℕ∞<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : M → 𝕜<VAR>g : M → V<VAR>hf : ContMDiff I 𝓘(𝕜, 𝕜) n f<VAR>hg : ContMDiff I 𝓘(𝕜, V) n g<GOAL>ContMDiff I 𝓘(𝕜, V) n fun p => f p • g p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>x : M<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : M → 𝕜<VAR>g : M → V<VAR>hf : SmoothWithinAt I 𝓘(𝕜, 𝕜) f s x<VAR>hg : SmoothWithinAt I 𝓘(𝕜, V) g s x<GOAL>SmoothWithinAt I 𝓘(𝕜, V) (fun p => f p • g p) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : M → 𝕜<VAR>g : M → V<VAR>hf : SmoothAt I 𝓘(𝕜, 𝕜) f x<VAR>hg : SmoothAt I 𝓘(𝕜, V) g x<GOAL>SmoothAt I 𝓘(𝕜, V) (fun p => f p • g p) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : M → 𝕜<VAR>g : M → V<VAR>hf : SmoothOn I 𝓘(𝕜, 𝕜) f s<VAR>hg : SmoothOn I 𝓘(𝕜, V) g s<GOAL>SmoothOn I 𝓘(𝕜, V) (fun p => f p • g p) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>V : Type u_18<VAR>NormedAddCommGroup V<VAR>NormedSpace 𝕜 V<VAR>f : M → 𝕜<VAR>g : M → V<VAR>hf : Smooth I 𝓘(𝕜, 𝕜) f<VAR>hg : Smooth I 𝓘(𝕜, V) g<GOAL>Smooth I 𝓘(𝕜, V) fun p => f p • g p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>n : ℕ∞<VAR>f : E → H'<VAR>s : Set E<VAR>x : E<GOAL>ContDiffWithinAtProp 𝓘(𝕜, E) I' n f s x ↔ ContDiffWithinAt 𝕜 n (↑I' ∘ f) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>n : ℕ∞<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>ContDiffWithinAtProp 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>n : ℕ∞<VAR>f : H → E'<VAR>s : Set H<VAR>x : H<GOAL>ContDiffWithinAtProp I 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n (f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I) (↑I x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>n : ℕ∞<GOAL>(contDiffGroupoid ⊤ I).LocalInvariantProp (contDiffGroupoid ⊤ I') (ContDiffWithinAtProp I I' n)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>t : Set H<VAR>f : H → H'<VAR>hts : s ∈ 𝓝[t] x<VAR>h : ContDiffWithinAtProp I I' n f s x<GOAL>ContDiffWithinAtProp I I' n f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>n : ℕ∞<VAR>x : H<GOAL>ContDiffWithinAtProp I I n id Set.univ x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>f : M → M'<VAR>x : M<GOAL>ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>le : m ≤ n<GOAL>ContMDiffWithinAt I I' m f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffAt I I' n f x<VAR>le : m ≤ n<GOAL>ContMDiffAt I I' m f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>le : m ≤ n<GOAL>ContMDiffOn I I' m f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>m n : ℕ∞<VAR>hf : ContMDiff I I' n f<VAR>le : m ≤ n<GOAL>ContMDiff I I' m f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>h : ContMDiff I I' ⊤ f<GOAL>Smooth I I' f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>n : ℕ∞<VAR>h : Smooth I I' f<GOAL>ContMDiff I I' n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>h : ContMDiffOn I I' ⊤ f s<GOAL>SmoothOn I I' f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>h : SmoothOn I I' f s<GOAL>ContMDiffOn I I' n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>h : ContMDiffAt I I' ⊤ f x<GOAL>SmoothAt I I' f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>n : ℕ∞<VAR>h : SmoothAt I I' f x<GOAL>ContMDiffAt I I' n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>h : ContMDiffWithinAt I I' ⊤ f s x<GOAL>SmoothWithinAt I I' f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>h : SmoothWithinAt I I' f s x<GOAL>ContMDiffWithinAt I I' n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>n : ℕ∞<VAR>h : ContMDiff I I' n f<GOAL>ContMDiffAt I I' n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>h : Smooth I I' f<GOAL>SmoothAt I I' f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f Set.univ x ↔ ContMDiffAt I I' n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<GOAL>SmoothWithinAt I I' f Set.univ x ↔ SmoothAt I I' f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>n : ℕ∞<GOAL>ContMDiffOn I I' n f Set.univ ↔ ContMDiff I I' n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<GOAL>SmoothOn I I' f Set.univ ↔ Smooth I I' f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (↑(extChartAt I' (f x)) ∘ f) s x