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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>z : M<VAR>f : M → E'<VAR>hf : MDifferentiableAt I 𝓘(𝕜, E') f z<VAR>s : 𝕜<GOAL>mfderiv I 𝓘(𝕜, E') (s • f) z = s • mfderiv I 𝓘(𝕜, E') f z
<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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>z : M<VAR>f : M → E'<VAR>f' : TangentSpace I z →L[𝕜] E'<VAR>hf : HasMFDerivAt I 𝓘(𝕜, E') f z f'<GOAL>HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>z : M<VAR>f : M → E'<VAR>f' : TangentSpace I z →L[𝕜] E'<GOAL>HasMFDerivAt I 𝓘(𝕜, E') (-f) z (-f') ↔ HasMFDerivAt I 𝓘(𝕜, E') f z 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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>z : M<VAR>f : M → E'<VAR>hf : MDifferentiableAt I 𝓘(𝕜, E') f z<GOAL>MDifferentiableAt I 𝓘(𝕜, E') (-f) z
<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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>z : M<VAR>f : M → E'<GOAL>MDifferentiableAt I 𝓘(𝕜, E') (-f) z ↔ MDifferentiableAt I 𝓘(𝕜, E') f z
<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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : M → E'<VAR>hf : MDifferentiable I 𝓘(𝕜, E') f<GOAL>MDifferentiable I 𝓘(𝕜, E') (-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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f : M → E'<VAR>x : M<GOAL>mfderiv I 𝓘(𝕜, E') (-f) x = -mfderiv I 𝓘(𝕜, E') 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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>z : M<VAR>f g : M → E'<VAR>f' g' : TangentSpace I z →L[𝕜] E'<VAR>hf : HasMFDerivAt I 𝓘(𝕜, E') f z f'<VAR>hg : HasMFDerivAt I 𝓘(𝕜, E') g z g'<GOAL>HasMFDerivAt I 𝓘(𝕜, E') (f - g) z (f' - g')
<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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>z : M<VAR>f g : M → E'<VAR>hf : MDifferentiableAt I 𝓘(𝕜, E') f z<VAR>hg : MDifferentiableAt I 𝓘(𝕜, E') g z<GOAL>MDifferentiableAt I 𝓘(𝕜, E') (f - g) z
<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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>f g : M → E'<VAR>hf : MDifferentiable I 𝓘(𝕜, E') f<VAR>hg : MDifferentiable I 𝓘(𝕜, E') g<GOAL>MDifferentiable I 𝓘(𝕜, E') (f - g)
<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>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>z : M<VAR>f g : M → E'<VAR>hf : MDifferentiableAt I 𝓘(𝕜, E') f z<VAR>hg : MDifferentiableAt I 𝓘(𝕜, E') g z<GOAL>mfderiv I 𝓘(𝕜, E') (f - g) z = mfderiv I 𝓘(𝕜, E') f z - mfderiv I 𝓘(𝕜, E') g z
<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>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>z : M<VAR>F' : Type u_11<VAR>NormedRing F'<VAR>NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>p' q' : TangentSpace I z →L[𝕜] F'<VAR>hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'<VAR>hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'<GOAL>HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + p'.smulRight (q z))
<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>SmoothManifoldWithCorners I M<VAR>z : M<VAR>F' : Type u_11<VAR>NormedRing F'<VAR>NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>p' q' : TangentSpace I z →L[𝕜] F'<VAR>hp : HasMFDerivAt I 𝓘(𝕜, F') p z p'<VAR>hq : HasMFDerivAt I 𝓘(𝕜, F') q z q'<GOAL>HasMFDerivAt I 𝓘(𝕜, F') (p * q) z (p z • q' + p'.smulRight (q z))
<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>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>z : M<VAR>F' : Type u_11<VAR>NormedRing F'<VAR>NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>hp : MDifferentiableWithinAt I 𝓘(𝕜, F') p s z<VAR>hq : MDifferentiableWithinAt I 𝓘(𝕜, F') q s z<GOAL>MDifferentiableWithinAt I 𝓘(𝕜, F') (p * q) s z
<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>SmoothManifoldWithCorners I M<VAR>z : M<VAR>F' : Type u_11<VAR>NormedRing F'<VAR>NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>hp : MDifferentiableAt I 𝓘(𝕜, F') p z<VAR>hq : MDifferentiableAt I 𝓘(𝕜, F') q z<GOAL>MDifferentiableAt I 𝓘(𝕜, F') (p * q) z
<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>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>F' : Type u_11<VAR>NormedRing F'<VAR>NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>hp : MDifferentiableOn I 𝓘(𝕜, F') p s<VAR>hq : MDifferentiableOn I 𝓘(𝕜, F') q s<GOAL>MDifferentiableOn I 𝓘(𝕜, F') (p * q) 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>SmoothManifoldWithCorners I M<VAR>F' : Type u_11<VAR>NormedRing F'<VAR>NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>hp : MDifferentiable I 𝓘(𝕜, F') p<VAR>hq : MDifferentiable I 𝓘(𝕜, F') q<GOAL>MDifferentiable I 𝓘(𝕜, F') (p * q)
<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>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>z : M<VAR>F' : Type u_11<VAR>NormedCommRing F'<VAR>NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>p' q' : TangentSpace I z →L[𝕜] F'<VAR>hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'<VAR>hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'<GOAL>HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + q z • 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>SmoothManifoldWithCorners I M<VAR>z : M<VAR>F' : Type u_11<VAR>NormedCommRing F'<VAR>NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>p' q' : TangentSpace I z →L[𝕜] F'<VAR>hp : HasMFDerivAt I 𝓘(𝕜, F') p z p'<VAR>hq : HasMFDerivAt I 𝓘(𝕜, F') q z q'<GOAL>HasMFDerivAt I 𝓘(𝕜, F') (p * q) z (p z • q' + q z • p')
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>N : Type u<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ<GOAL>(smoothSheaf IM I M N).presheaf.obj U = ContMDiffMap IM I (↥(Opposite.unop U)) N ⊤
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>N : Type u<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>x : ↑(TopCat.of M)<VAR>U : (TopologicalSpace.OpenNhds x)ᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).val) U) (smoothSheaf.evalHom IM I N x) = smoothSheaf.evalAt IM I N x (Opposite.unop U)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>N : Type u<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>x : M<GOAL>Function.Surjective (smoothSheaf.eval IM I N x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>N : Type u<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>U : TopologicalSpace.Opens M<VAR>x : ↥U<VAR>f : (smoothSheaf IM I M N).presheaf.obj (Opposite.op U)<GOAL>smoothSheaf.eval IM I N (↑x) ((smoothSheaf IM I M N).presheaf.germ x f) = ↑f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>N : Type u<VAR>TopologicalSpace N<VAR>ChartedSpace H N<VAR>U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ<VAR>f : (smoothSheaf IM I M N).presheaf.obj U<GOAL>Smooth IM I ↑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>R : Type u<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>CommRing R<VAR>SmoothRing I R<VAR>x : ↑(TopCat.of M)<VAR>U : (TopologicalSpace.OpenNhds x)ᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp (⇑(CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)) (smoothSheafCommRing.forgetStalk IM I M R x).hom = CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf) U
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>R : Type u<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>CommRing R<VAR>SmoothRing I R<VAR>x : ↑(TopCat.of M)<VAR>U : (TopologicalSpace.OpenNhds x)ᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf) U) (smoothSheafCommRing.forgetStalk IM I M R x).inv = (CategoryTheory.forget CommRingCat).map (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>R : Type u<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>CommRing R<VAR>SmoothRing I R<VAR>x : ↑(TopCat.of M)<VAR>U : (TopologicalSpace.OpenNhds x)ᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U) (smoothSheafCommRing.evalHom IM I M R x) = smoothSheafCommRing.evalAt IM I M R x (Opposite.unop U)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>R : Type u<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>CommRing R<VAR>SmoothRing I R<VAR>U : TopologicalSpace.Opens ↑(TopCat.of M)<VAR>x : ↥U<VAR>f : ↑((smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U))<GOAL>(smoothSheafCommRing.evalHom IM I M R ↑x) (((smoothSheafCommRing IM I M R).presheaf.germ x) f) = ↑f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>R : Type u<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>CommRing R<VAR>SmoothRing I R<VAR>x : ↑(TopCat.of M)<GOAL>CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).inv ⇑(smoothSheafCommRing.evalHom IM I M R x) = smoothSheaf.evalHom IM I R x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>R : Type u<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>CommRing R<VAR>SmoothRing I R<VAR>x : ↑(TopCat.of M)<GOAL>CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).hom (smoothSheaf.evalHom IM I R x) = (CategoryTheory.forget CommRingCat).map (smoothSheafCommRing.evalHom IM I M R x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>R : Type u<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>CommRing R<VAR>SmoothRing I R<VAR>x : M<GOAL>Function.Surjective ⇑(smoothSheafCommRing.eval IM I M R x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>R : Type u<VAR>TopologicalSpace R<VAR>ChartedSpace H R<VAR>CommRing R<VAR>SmoothRing I R<VAR>U : TopologicalSpace.Opens M<VAR>x : ↥U<VAR>f : ↑((smoothSheafCommRing IM I M R).presheaf.obj (Opposite.op U))<GOAL>(smoothSheafCommRing.eval IM I M R ↑x) (((smoothSheafCommRing IM I M R).presheaf.germ x) f) = ↑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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>hg : ContMDiffWithinAt I' I'' n g t (f x)<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>st : Set.MapsTo f s t<GOAL>ContMDiffWithinAt I I'' n (g ∘ 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>y : M'<VAR>hg : ContMDiffWithinAt I' I'' n g t y<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>st : Set.MapsTo f s t<VAR>hx : f x = y<GOAL>ContMDiffWithinAt I I'' n (g ∘ 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>s : Set M<VAR>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>hg : SmoothWithinAt I' I'' g t (f x)<VAR>hf : SmoothWithinAt I I' f s x<VAR>st : Set.MapsTo f s t<GOAL>SmoothWithinAt I I'' (g ∘ 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>hg : ContMDiffOn I' I'' n g t<VAR>hf : ContMDiffOn I I' n f s<VAR>st : s ⊆ f ⁻¹' t<GOAL>ContMDiffOn I I'' n (g ∘ 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>s : Set M<VAR>t : Set M'<VAR>g : M' → M''<VAR>hg : SmoothOn I' I'' g t<VAR>hf : SmoothOn I I' f s<VAR>st : s ⊆ f ⁻¹' t<GOAL>SmoothOn I I'' (g ∘ 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>TopologicalSpace M''<VAR>ChartedSpace H'' M''<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>t : Set M'<VAR>g : M' → M''<VAR>hg : ContMDiffOn I' I'' n g t<VAR>hf : ContMDiffOn I I' n f s<GOAL>ContMDiffOn I I'' n (g ∘ f) (s ∩ f ⁻¹' t)