ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>x : M<VAR>hf : SmoothWithinAt IM IB f s x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>SmoothWithinAt IM 𝓘(𝕜, F →L[𝕜] F) (fun y => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) s x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>f : M → B<VAR>x : M<VAR>hf : SmoothAt IM IB f x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>SmoothAt IM 𝓘(𝕜, F →L[𝕜] F) (fun y => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>hf : SmoothOn IM IB f s<VAR>he : Set.MapsTo f s e.baseSet<VAR>he' : Set.MapsTo f s e'.baseSet<GOAL>SmoothOn IM 𝓘(𝕜, F →L[𝕜] F) (fun y => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))) s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>f : M → B<VAR>hf : Smooth IM IB f<VAR>he : ∀ (x : M), f x ∈ e.baseSet<VAR>he' : ∀ (x : M), f x ∈ e'.baseSet<GOAL>Smooth IM 𝓘(𝕜, F →L[𝕜] F) fun y => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>hf : ContMDiffWithinAt IM IB n f s x<VAR>hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => e.coordChange e' (f y) (g y)) s x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>hf : ContMDiffAt IM IB n f x<VAR>hg : ContMDiffAt IM 𝓘(𝕜, F) n g x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>ContMDiffAt IM 𝓘(𝕜, F) n (fun y => e.coordChange e' (f y) (g y)) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>hf : ContMDiffOn IM IB n f s<VAR>hg : ContMDiffOn IM 𝓘(𝕜, F) n g s<VAR>he : Set.MapsTo f s e.baseSet<VAR>he' : Set.MapsTo f s e'.baseSet<GOAL>ContMDiffOn IM 𝓘(𝕜, F) n (fun y => e.coordChange e' (f y) (g y)) s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>f : M → B<VAR>g : M → F<VAR>hf : ContMDiff IM IB n f<VAR>hg : ContMDiff IM 𝓘(𝕜, F) n g<VAR>he : ∀ (x : M), f x ∈ e.baseSet<VAR>he' : ∀ (x : M), f x ∈ e'.baseSet<GOAL>ContMDiff IM 𝓘(𝕜, F) n fun y => e.coordChange e' (f y) (g y)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>hf : SmoothWithinAt IM IB f s x<VAR>hg : SmoothWithinAt IM 𝓘(𝕜, F) g s x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>SmoothWithinAt IM 𝓘(𝕜, F) (fun y => e.coordChange e' (f y) (g y)) s x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>f : M → B<VAR>g : M → F<VAR>x : M<VAR>hf : SmoothAt IM IB f x<VAR>hg : SmoothAt IM 𝓘(𝕜, F) g x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>SmoothAt IM 𝓘(𝕜, F) (fun y => e.coordChange e' (f y) (g y)) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>s : Set M<VAR>f : M → B<VAR>g : M → F<VAR>hf : SmoothOn IM IB f s<VAR>hg : SmoothOn IM 𝓘(𝕜, F) g s<VAR>he : Set.MapsTo f s e.baseSet<VAR>he' : Set.MapsTo f s e'.baseSet<GOAL>SmoothOn IM 𝓘(𝕜, F) (fun y => e.coordChange e' (f y) (g y)) s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>f : M → B<VAR>g : M → F<VAR>hf : Smooth IM IB f<VAR>hg : Smooth IM 𝓘(𝕜, F) g<VAR>he : ∀ (x : M), f x ∈ e.baseSet<VAR>he' : ∀ (x : M), f x ∈ e'.baseSet<GOAL>Smooth IM 𝓘(𝕜, F) fun y => e.coordChange e' (f y) (g y)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<GOAL>ContMDiffOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) n (↑(e.symm ≫ₕ e'.toPartialHomeomorph)) (e.target ∩ e'.target)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>s : Set M<VAR>x : M<VAR>f : M → Bundle.TotalSpace F E<VAR>hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x<VAR>hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e (f y)).2) s x<VAR>he : f x ∈ e.source<VAR>he' : f x ∈ e'.source<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e' (f y)).2) s x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<VAR>s : Set M<VAR>x : M<VAR>f : M → Bundle.TotalSpace F E<VAR>hp : ContMDiffWithinAt IM IB n (Bundle.TotalSpace.proj ∘ f) s x<VAR>he : f x ∈ e.source<VAR>he' : f x ∈ e'.source<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e (f y)).2) s x ↔ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e' (f y)).2) s x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>f : M → Bundle.TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<VAR>he : f x₀ ∈ e.source<GOAL>ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x₀ ↔ ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x => (↑e (f x)).2) s x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>f : M → Bundle.TotalSpace F E<VAR>x₀ : M<VAR>he : f x₀ ∈ e.source<GOAL>ContMDiffAt IM (IB.prod 𝓘(𝕜, F)) n f x₀ ↔ ContMDiffAt IM IB n (fun x => (f x).proj) x₀ ∧ ContMDiffAt IM 𝓘(𝕜, F) n (fun x => (↑e (f x)).2) x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>f : M → Bundle.TotalSpace F E<VAR>s : Set M<VAR>he : Set.MapsTo f s e.source<GOAL>ContMDiffOn IM (IB.prod 𝓘(𝕜, F)) n f s ↔ ContMDiffOn IM IB n (fun x => (f x).proj) s ∧ ContMDiffOn IM 𝓘(𝕜, F) n (fun x => (↑e (f x)).2) s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>f : M → Bundle.TotalSpace F E<VAR>he : ∀ (x : M), f x ∈ e.source<GOAL>ContMDiff IM (IB.prod 𝓘(𝕜, F)) n f ↔ (ContMDiff IM IB n fun x => (f x).proj) ∧ ContMDiff IM 𝓘(𝕜, F) n fun x => (↑e (f x)).2
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>f : M → Bundle.TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<VAR>he : f x₀ ∈ e.source<GOAL>SmoothWithinAt IM (IB.prod 𝓘(𝕜, F)) f s x₀ ↔ SmoothWithinAt IM IB (fun x => (f x).proj) s x₀ ∧ SmoothWithinAt IM 𝓘(𝕜, F) (fun x => (↑e (f x)).2) s x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>f : M → Bundle.TotalSpace F E<VAR>x₀ : M<VAR>he : f x₀ ∈ e.source<GOAL>SmoothAt IM (IB.prod 𝓘(𝕜, F)) f x₀ ↔ SmoothAt IM IB (fun x => (f x).proj) x₀ ∧ SmoothAt IM 𝓘(𝕜, F) (fun x => (↑e (f x)).2) x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>NormedAddCommGroup EB<VAR>NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>EM : Type u_9<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>FiberBundle F E<VAR>VectorBundle 𝕜 F E<VAR>SmoothVectorBundle F E IB<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>f : M → Bundle.TotalSpace F E<VAR>s : Set M<VAR>he : Set.MapsTo f s e.source<GOAL>SmoothOn IM (IB.prod 𝓘(𝕜, F)) f s ↔ SmoothOn IM IB (fun x => (f x).proj) s ∧ SmoothOn IM 𝓘(𝕜, F) (fun x => (↑e (f x)).2) s