ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.SheafedSpace C<VAR>f : U ⟶ ↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<GOAL>(X.ofRestrict h).base = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.SheafedSpace C<GOAL>X.restrictTopIso.inv = X.toRestrictTop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.SheafedSpace C<GOAL>X.restrictTopIso.hom = X.ofRestrict ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>AlgebraicGeometry.SheafedSpace.Γ = AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.op ⋙ AlgebraicGeometry.PresheafedSpace.Γ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ<GOAL>AlgebraicGeometry.SheafedSpace.Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.SheafedSpace C<GOAL>AlgebraicGeometry.SheafedSpace.Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : (AlgebraicGeometry.SheafedSpace C)ᵒᵖ<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.SheafedSpace.Γ.map f = f.unop.c.app (Opposite.op ⊤)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.SheafedSpace.Γ.map f.op = f.c.app (Opposite.op ⊤)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f g : X ⟶ Y<VAR>h : f.base = g.base<VAR>h' : ∀ (x : ↑↑X.toPresheafedSpace), AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x = (Y.presheaf.stalkCongr ⋯).hom ≫ AlgebraicGeometry.PresheafedSpace.Hom.stalkMap g x<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>h₁ : Function.Injective ⇑f.base<VAR>h₂ : ∀ (x : ↑↑X.toPresheafedSpace), CategoryTheory.Epi (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x)<GOAL>CategoryTheory.Mono f
<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>TopologicalSpace B<VAR>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<GOAL>chartAt (B × F) x = (trivializationAt F E x.proj).toPartialHomeomorph
<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>HB : Type u_7<VAR>TopologicalSpace HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<GOAL>chartAt (ModelProd HB F) x = (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (PartialHomeomorph.refl F)
<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<VAR>HB : Type u_7<VAR>TopologicalSpace HB<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<VAR>y : ModelProd HB F<VAR>hy : y ∈ (chartAt (ModelProd HB F) x).target<GOAL>(↑(chartAt (ModelProd HB F) x).symm y).proj = ↑(chartAt HB x.proj).symm y.1
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<GOAL>extChartAt (IB.prod 𝓘(𝕜, F)) x = (trivializationAt F E x.proj).toPartialEquiv ≫ (extChartAt IB x.proj).prod (PartialEquiv.refl F)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<GOAL>(extChartAt (IB.prod 𝓘(𝕜, F)) x).target = ((extChartAt IB x.proj).target ∩ ↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ Set.univ
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<VAR>y : EB × F<VAR>hy : y ∈ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target<GOAL>writtenInExtChartAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) x (↑(trivializationAt F E x.proj)) y = y
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<VAR>x : Bundle.TotalSpace F E<VAR>y : EB × F<VAR>hy : y ∈ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target<GOAL>writtenInExtChartAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) (↑(trivializationAt F E x.proj) x) (↑(trivializationAt F E x.proj).symm) y = 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>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>EM : Type u_10<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<VAR>f : M → Bundle.TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<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 => (↑(trivializationAt F E (f x₀).proj) (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>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>EM : Type u_10<VAR>NormedAddCommGroup EM<VAR>NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>TopologicalSpace M<VAR>ChartedSpace HM M<VAR>n : ℕ∞<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<VAR>f : M → Bundle.TotalSpace F E<VAR>x₀ : M<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 => (↑(trivializationAt F E (f x₀).proj) (f x)).2) x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>n : ℕ∞<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<VAR>s : (x : B) → E x<VAR>x₀ : B<GOAL>ContMDiffAt IB (IB.prod 𝓘(𝕜, F)) n (fun x => Bundle.TotalSpace.mk' F x (s x)) x₀ ↔ ContMDiffAt IB 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F E x₀) { proj := x, snd := s x }).2) x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>n : ℕ∞<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<GOAL>ContMDiff (IB.prod 𝓘(𝕜, F)) IB n Bundle.TotalSpace.proj
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<GOAL>Smooth (IB.prod 𝓘(𝕜, F)) IB Bundle.TotalSpace.proj
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>n : ℕ∞<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<VAR>s : Set (Bundle.TotalSpace F E)<GOAL>ContMDiffOn (IB.prod 𝓘(𝕜, F)) IB n Bundle.TotalSpace.proj s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<VAR>s : Set (Bundle.TotalSpace F E)<GOAL>SmoothOn (IB.prod 𝓘(𝕜, F)) IB Bundle.TotalSpace.proj s
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>n : ℕ∞<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<VAR>p : Bundle.TotalSpace F E<GOAL>ContMDiffAt (IB.prod 𝓘(𝕜, F)) IB n Bundle.TotalSpace.proj p
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<VAR>p : Bundle.TotalSpace F E<GOAL>SmoothAt (IB.prod 𝓘(𝕜, F)) IB Bundle.TotalSpace.proj p
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>n : ℕ∞<VAR>TopologicalSpace B<VAR>ChartedSpace HB B<VAR>FiberBundle F E<VAR>s : Set (Bundle.TotalSpace F E)<VAR>p : Bundle.TotalSpace F E<GOAL>ContMDiffWithinAt (IB.prod 𝓘(𝕜, F)) IB n Bundle.TotalSpace.proj s p
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<VAR>s : Set (Bundle.TotalSpace F E)<VAR>p : Bundle.TotalSpace F E<GOAL>SmoothWithinAt (IB.prod 𝓘(𝕜, F)) IB Bundle.TotalSpace.proj s p
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_4<VAR>E : B → Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → TopologicalSpace (E x)<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>FiberBundle F E<VAR>(x : B) → AddCommMonoid (E x)<VAR>(x : B) → Module 𝕜 (E x)<VAR>VectorBundle 𝕜 F E<GOAL>Smooth IB (IB.prod 𝓘(𝕜, F)) (Bundle.zeroSection F E)
<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>(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>self : SmoothVectorBundle F E IB<VAR>e e' : Trivialization F Bundle.TotalSpace.proj<VAR>MemTrivializationAtlas e<VAR>MemTrivializationAtlas e'<GOAL>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
<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>(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>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
<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>(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>SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b).symm) (e.baseSet ∩ e'.baseSet)
<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 𝓘(𝕜, F →L[𝕜] F) n (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) (e.baseSet ∩ e'.baseSet)
<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 𝓘(𝕜, F →L[𝕜] F) n (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b).symm) (e.baseSet ∩ e'.baseSet)
<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'<VAR>x : B<VAR>h : x ∈ e.baseSet<VAR>h' : x ∈ e'.baseSet<GOAL>ContMDiffAt IB 𝓘(𝕜, F →L[𝕜] F) n (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) x
<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>(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>x : B<VAR>h : x ∈ e.baseSet<VAR>h' : x ∈ e'.baseSet<GOAL>SmoothAt IB 𝓘(𝕜, F →L[𝕜] F) (fun b => ↑(Trivialization.coordChangeL 𝕜 e e' b)) 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>x : M<VAR>hf : ContMDiffWithinAt IM IB n f s x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, F →L[𝕜] F) n (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>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>x : M<VAR>hf : ContMDiffAt IM IB n f x<VAR>he : f x ∈ e.baseSet<VAR>he' : f x ∈ e'.baseSet<GOAL>ContMDiffAt IM 𝓘(𝕜, F →L[𝕜] F) n (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>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>hf : ContMDiffOn IM IB n f s<VAR>he : Set.MapsTo f s e.baseSet<VAR>he' : Set.MapsTo f s e'.baseSet<GOAL>ContMDiffOn IM 𝓘(𝕜, F →L[𝕜] F) n (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>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>hf : ContMDiff IM IB n f<VAR>he : ∀ (x : M), f x ∈ e.baseSet<VAR>he' : ∀ (x : M), f x ∈ e'.baseSet<GOAL>ContMDiff IM 𝓘(𝕜, F →L[𝕜] F) n fun y => ↑(Trivialization.coordChangeL 𝕜 e e' (f y))