ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_4<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>GroupWithZero G<VAR>SmoothInv₀ I G<VAR>SmoothMul I G<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 g : M → G<VAR>hf : Smooth I' I f<VAR>hg : Smooth I' I g<VAR>h₀ : ∀ (x : M), g x ≠ 0<GOAL>Smooth I' I (f / g)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>i j : ↑(atlas H M)<GOAL>ContDiffOn 𝕜 ⊤ (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (Set.range ↑I)) (((↑i).extend I).symm ≫ (↑j).extend I).source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>i j : ↑(atlas H M)<VAR>x : M<GOAL>(tangentBundleCore I M).coordChange i j x = fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (Set.range ↑I) (↑((↑i).extend I) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>(tangentBundleCore I M).indexAt x = achart H x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>i : ↑(atlas H M)<GOAL>(tangentBundleCore I M).baseSet i = (↑i).source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x x' z : M<GOAL>(tangentBundleCore I M).coordChange (achart H x) (achart H x') z = fderivWithin 𝕜 (↑(extChartAt I x') ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) z)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x y z : M<GOAL>tangentCoordChange I x y z = fderivWithin 𝕜 (↑(extChartAt I y) ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) z)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x z : M<VAR>v : E<VAR>h : z ∈ (extChartAt I x).source<GOAL>(tangentCoordChange I x x z) v = v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>w x y z : M<VAR>v : E<VAR>h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source<GOAL>(tangentCoordChange I x y z) ((tangentCoordChange I w x z) v) = (tangentCoordChange I w y z) v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x y z : M<VAR>h : z ∈ (extChartAt I x).source ∩ (extChartAt I y).source<GOAL>HasFDerivWithinAt (↑(extChartAt I y) ∘ ↑(extChartAt I x).symm) (tangentCoordChange I x y z) (Set.range ↑I) (↑(extChartAt I x) z)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x y : M<GOAL>ContinuousOn (tangentCoordChange I x y) ((extChartAt I x).source ∩ (extChartAt I y).source)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>p : TangentBundle I M<GOAL>chartAt (ModelProd H E) p = ((tangentBundleCore I M).toFiberBundleCore.localTriv (achart H p.proj)).toPartialHomeomorph ≫ₕ (chartAt H p.proj).prod (PartialHomeomorph.refl E)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>p : TangentBundle I M<GOAL>(chartAt (ModelProd H E) p).toPartialEquiv = (tangentBundleCore I M).toFiberBundleCore.localTrivAsPartialEquiv (achart H p.proj) ≫ (chartAt H p.proj).prod (PartialEquiv.refl E)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>trivializationAt E (TangentSpace I) x = (tangentBundleCore I M).toFiberBundleCore.localTriv (achart H x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>(trivializationAt E (TangentSpace I) x).source = Bundle.TotalSpace.proj ⁻¹' (chartAt H x).source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>(trivializationAt E (TangentSpace I) x).target = (chartAt H x).source ×ˢ Set.univ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<GOAL>(trivializationAt E (TangentSpace I) x).baseSet = (chartAt H x).source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<VAR>z : TangentBundle I M<GOAL>↑(trivializationAt E (TangentSpace I) x) z = (z.proj, (fderivWithin 𝕜 (↑((chartAt H x).extend I) ∘ ↑((chartAt H z.proj).extend I).symm) (Set.range ↑I) (↑((chartAt H z.proj).extend I) z.proj)) z.snd)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>x : M<VAR>z : TangentBundle I M<GOAL>(↑(trivializationAt E (TangentSpace I) x) z).1 = z.proj
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>p q : TangentBundle I M<GOAL>p ∈ (chartAt (ModelProd H E) q).source ↔ p.proj ∈ (chartAt H q.proj).source
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>p : H × E<VAR>q : TangentBundle I M<GOAL>p ∈ (chartAt (ModelProd H E) q).target ↔ p.1 ∈ (chartAt H q.proj).target
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>p q : TangentBundle I M<GOAL>(↑(chartAt (ModelProd H E) q) p).1 = ↑(chartAt H q.proj) p.proj
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>p : H × E<VAR>q : TangentBundle I M<GOAL>(↑(chartAt (ModelProd H E) q).symm p).proj = ↑(chartAt H q.proj).symm p.1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>b₀ b : M<VAR>hb : b ∈ (trivializationAt E (TangentSpace I) b₀).baseSet<GOAL>Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) b₀) b = (tangentBundleCore I M).coordChange (achart H b) (achart H b₀) b
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>b₀ b : M<VAR>hb : b ∈ (trivializationAt E (TangentSpace I) b₀).baseSet<GOAL>Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) b₀) b = (tangentBundleCore I M).coordChange (achart H b₀) (achart H b) b
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>b b' x : F<GOAL>(tangentBundleCore 𝓘(𝕜, F) F).coordChange (achart F b) (achart F b') x = 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>b b' : F<GOAL>Trivialization.symmL 𝕜 (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b' = 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>b b' : F<GOAL>Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F (TangentSpace 𝓘(𝕜, F)) b) b' = 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>p : TangentBundle I H<GOAL>(chartAt (ModelProd H E) p).toPartialEquiv = (Bundle.TotalSpace.toProd H E).toPartialEquiv
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>p : TangentBundle I H<GOAL>↑(chartAt (ModelProd H E) p) = ⇑(Bundle.TotalSpace.toProd H E)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>p : TangentBundle I H<GOAL>↑(chartAt (ModelProd H E) p).symm = ⇑(Bundle.TotalSpace.toProd H E).symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>x x' z : H<GOAL>(tangentBundleCore I H).coordChange (achart H x) (achart H x') z = ContinuousLinearMap.id 𝕜 E
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>⇑(tangentBundleModelSpaceHomeomorph H I) = ⇑(Bundle.TotalSpace.toProd H E)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<GOAL>⇑(tangentBundleModelSpaceHomeomorph H I).symm = ⇑(Bundle.TotalSpace.toProd H E).symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>x₀ x : H<VAR>y₀ y : H'<VAR>ϕ : E →L[𝕜] E'<GOAL>ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>N : Type u_9<VAR>f : N → H<VAR>g : N → H'<VAR>ϕ : N → E →L[𝕜] E'<VAR>x₀ : N<GOAL>inTangentCoordinates I I' f g ϕ x₀ = ϕ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>N : Type u_9<VAR>f : N → M<VAR>g : N → M'<VAR>ϕ : N → E →L[𝕜] E'<VAR>x₀ x : N<VAR>hx : f x ∈ (chartAt H (f x₀)).source<VAR>hy : g x ∈ (chartAt H' (g x₀)).source<GOAL>inTangentCoordinates I I' f g ϕ x₀ x = ((tangentBundleCore I' M').coordChange (achart H' (g x)) (achart H' (g x₀)) (g x)).comp ((ϕ x).comp ((tangentBundleCore I M).coordChange (achart H (f x₀)) (achart H (f x)) (f x)))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>self : Cₛ^n⟮I; F, V⟯<GOAL>ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x => Bundle.TotalSpace.mk' F x (self.toFun x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>s : (x : M) → V x<VAR>hs : ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x => { proj := x, snd := s x }<GOAL>⇑{ toFun := s, contMDiff_toFun := hs } = s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>s : Cₛ^n⟮I; F, V⟯<GOAL>ContMDiff I (I.prod 𝓘(𝕜, F)) n fun x => Bundle.TotalSpace.mk' 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_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>s : Cₛ^⊤⟮I; F, V⟯<GOAL>Smooth I (I.prod 𝓘(𝕜, F)) fun x => Bundle.TotalSpace.mk' 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_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>s : Cₛ^n⟮I; F, V⟯<VAR>hn : 1 ≤ n<GOAL>MDifferentiable I (I.prod 𝓘(𝕜, F)) fun x => Bundle.TotalSpace.mk' 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_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>s : Cₛ^⊤⟮I; F, V⟯<GOAL>MDifferentiable I (I.prod 𝓘(𝕜, F)) fun x => Bundle.TotalSpace.mk' 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_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>s : Cₛ^⊤⟮I; F, V⟯<VAR>x : M<GOAL>MDifferentiableAt I (I.prod 𝓘(𝕜, F)) (fun x => Bundle.TotalSpace.mk' F x (s x)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>s t : Cₛ^n⟮I; F, V⟯<VAR>h : ⇑s = ⇑t<GOAL>s = t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<GOAL>Function.Injective DFunLike.coe
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>s t : Cₛ^n⟮I; F, V⟯<VAR>h : ∀ (x : M), s x = t x<GOAL>s = t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → AddCommGroup (V x)<VAR>(x : M) → Module 𝕜 (V x)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>VectorBundle 𝕜 F V<VAR>s t : Cₛ^n⟮I; F, V⟯<GOAL>⇑(s + t) = ⇑s + ⇑t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → AddCommGroup (V x)<VAR>(x : M) → Module 𝕜 (V x)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>VectorBundle 𝕜 F V<VAR>s t : Cₛ^n⟮I; F, V⟯<GOAL>⇑(s - t) = ⇑s - ⇑t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → AddCommGroup (V x)<VAR>(x : M) → Module 𝕜 (V x)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>VectorBundle 𝕜 F V<GOAL>⇑0 = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → AddCommGroup (V x)<VAR>(x : M) → Module 𝕜 (V x)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>VectorBundle 𝕜 F V<VAR>r : 𝕜<VAR>s : Cₛ^n⟮I; F, V⟯<GOAL>⇑(r • s) = r • ⇑s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → AddCommGroup (V x)<VAR>(x : M) → Module 𝕜 (V x)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>VectorBundle 𝕜 F V<VAR>s : Cₛ^n⟮I; F, V⟯<GOAL>⇑(-s) = -⇑s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → AddCommGroup (V x)<VAR>(x : M) → Module 𝕜 (V x)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>VectorBundle 𝕜 F V<VAR>s : Cₛ^n⟮I; F, V⟯<VAR>k : ℕ<GOAL>⇑(k • s) = k • ⇑s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_4<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_6<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>F : Type u_11<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>V : M → Type u_12<VAR>TopologicalSpace (Bundle.TotalSpace F V)<VAR>(x : M) → AddCommGroup (V x)<VAR>(x : M) → Module 𝕜 (V x)<VAR>(x : M) → TopologicalSpace (V x)<VAR>FiberBundle F V<VAR>VectorBundle 𝕜 F V<VAR>s : Cₛ^n⟮I; F, V⟯<VAR>z : ℤ<GOAL>⇑(z • s) = z • ⇑s