ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>e : X ≅ Y<VAR>x : ↑X.toTopCat<VAR>y : ↑(X.presheaf.stalk (e.inv.val.base (e.hom.val.base x)))<GOAL>(AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom x) ((AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv (e.hom.val.base x)) y) = (X.presheaf.stalkSpecializes ⋯) y
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑Y.toTopCat<VAR>x : ↥((TopologicalSpace.Opens.map f.val.base).obj U)<GOAL>Y.presheaf.germ ⟨f.val.base ↑x, ⋯⟩ ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f ↑x = f.val.c.app (Opposite.op U) ≫ X.presheaf.germ x
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑Y.toTopCat<VAR>x : ↥((TopologicalSpace.Opens.map f.val.base).obj U)<VAR>y : ↑(Y.presheaf.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f ↑x) ((Y.presheaf.germ ⟨f.val.base ↑x, ⋯⟩) y) = (X.presheaf.germ x) ((f.val.c.app (Opposite.op U)) y)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑Y.toTopCat<VAR>x : ↑X.toTopCat<VAR>hx : f.val.base x ∈ U<GOAL>Y.presheaf.germ ⟨f.val.base x, hx⟩ ≫ AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x = f.val.c.app (Opposite.op U) ≫ X.presheaf.germ ⟨x, hx⟩
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑Y.toTopCat<VAR>x : ↑X.toTopCat<VAR>hx : f.val.base x ∈ U<VAR>y : ↑(Y.presheaf.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) ((Y.presheaf.germ ⟨f.val.base x, hx⟩) y) = (X.presheaf.germ ⟨x, hx⟩) ((f.val.c.app (Opposite.op U)) y)
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<VAR>V : TopologicalSpace.Opens ↑U<VAR>x : ↑U<VAR>hx : x ∈ V<GOAL>(X.restrict h).presheaf.germ ⟨x, hx⟩ ≫ (X.restrictStalkIso h x).hom = X.presheaf.germ ⟨f x, ⋯⟩
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<VAR>V : TopologicalSpace.Opens ↑U<VAR>x : ↑U<VAR>hx : x ∈ V<VAR>y : ↑((X.restrict h).presheaf.obj (Opposite.op V))<GOAL>(X.restrictStalkIso h x).hom (((X.restrict h).presheaf.germ ⟨x, hx⟩) y) = (X.presheaf.germ ⟨f x, ⋯⟩) y
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<VAR>V : TopologicalSpace.Opens ↑U<VAR>x : ↑U<VAR>hx : x ∈ V<GOAL>X.presheaf.germ ⟨f x, ⋯⟩ ≫ (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ ⟨x, hx⟩
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<VAR>V : TopologicalSpace.Opens ↑U<VAR>x : ↑U<VAR>hx : x ∈ V<VAR>y : ↑(X.presheaf.obj (Opposite.op (⋯.functor.obj V)))<GOAL>(X.restrictStalkIso h x).inv ((X.presheaf.germ ⟨f x, ⋯⟩) y) = ((X.restrict h).presheaf.germ ⟨x, hx⟩) y
<VAR>U : TopCat<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑U<GOAL>(X.restrictStalkIso h x).inv = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (X.ofRestrict h) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<GOAL>UniqueMDiffWithinAt I Set.univ x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>x : M<GOAL>UniqueMDiffWithinAt I s x ↔ UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s t : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : 𝓝[s] x ≤ 𝓝[t] x<GOAL>UniqueMDiffWithinAt I t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s t : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : t ∈ 𝓝[s] x<GOAL>UniqueMDiffWithinAt I t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>s t : Set M<VAR>h : UniqueMDiffWithinAt I s x<VAR>st : s ⊆ t<GOAL>UniqueMDiffWithinAt I t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>s t : Set M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : t ∈ 𝓝[s] x<GOAL>UniqueMDiffWithinAt I (s ∩ t) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>s t : Set M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : t ∈ 𝓝 x<GOAL>UniqueMDiffWithinAt I (s ∩ t) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>x : M<VAR>s : Set M<VAR>hs : IsOpen s<VAR>xs : x ∈ s<GOAL>UniqueMDiffWithinAt I 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>s t : Set M<VAR>hs : UniqueMDiffOn I s<VAR>ht : IsOpen t<GOAL>UniqueMDiffOn I (s ∩ t)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>hs : IsOpen s<GOAL>UniqueMDiffOn I 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<GOAL>UniqueMDiffOn I Set.univ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>U : UniqueMDiffWithinAt I s x<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>h₁ : HasMFDerivWithinAt I I' f s x f₁'<GOAL>f' = f₁'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>U : UniqueMDiffOn I s<VAR>hx : x ∈ s<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>h₁ : HasMFDerivWithinAt I I' f s x f₁'<GOAL>f' = f₁'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>x : M<VAR>y : M'<VAR>s : Set M<VAR>t : Set M'<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : UniqueMDiffWithinAt I' t y<GOAL>UniqueMDiffWithinAt (I.prod I') (s ×ˢ t) (x, y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>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>s : Set M<VAR>t : Set M'<VAR>hs : UniqueMDiffOn I s<VAR>ht : UniqueMDiffOn I' t<GOAL>UniqueMDiffOn (I.prod I') (s ×ˢ t)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<GOAL>MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>x' : M<VAR>y : M'<VAR>hx : x' ∈ (chartAt H x).source<VAR>hy : f x' ∈ (chartAt H' y).source<GOAL>MDifferentiableWithinAt I I' f s x' ↔ ContinuousWithinAt f s x' ∧ DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x')
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : ¬MDifferentiableWithinAt I I' f s x<GOAL>mfderivWithin I I' f s x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : ¬MDifferentiableAt I I' f x<GOAL>mfderiv I I' f x = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s t : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivWithinAt I I' f t x f'<VAR>hst : s ⊆ t<GOAL>HasMFDerivWithinAt I I' f s x f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivAt I I' f x f'<GOAL>HasMFDerivWithinAt I I' f s x f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivWithinAt I I' f s x f'<GOAL>MDifferentiableWithinAt I I' f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivAt I I' f x f'<GOAL>MDifferentiableAt I I' f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<GOAL>HasMFDerivWithinAt I I' f Set.univ x f' ↔ HasMFDerivAt I I' f x f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h₀ : HasMFDerivAt I I' f x f₀'<VAR>h₁ : HasMFDerivAt I I' f x f₁'<GOAL>f₀' = f₁'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s t : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : t ∈ 𝓝[s] x<GOAL>HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s t : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : t ∈ 𝓝 x<GOAL>HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s t : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>hs : HasMFDerivWithinAt I I' f s x f'<VAR>ht : HasMFDerivWithinAt I I' f t x f'<GOAL>HasMFDerivWithinAt I I' f (s ∪ t) x f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s t : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>ht : s ∈ 𝓝[t] x<GOAL>HasMFDerivWithinAt I I' f t x f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>hs : s ∈ 𝓝 x<GOAL>HasMFDerivAt I I' f x f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : MDifferentiableWithinAt I I' f s x<GOAL>HasMFDerivWithinAt I I' f s x (mfderivWithin I I' f s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : MDifferentiableWithinAt I I' f s x<GOAL>mfderivWithin I I' f s x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : MDifferentiableAt I I' f x<GOAL>HasMFDerivAt I I' f x (mfderiv I I' f x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : MDifferentiableAt I I' f x<GOAL>mfderiv I I' f x = fderivWithin 𝕜 (writtenInExtChartAt I I' x f) (Set.range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivAt I I' f x f'<GOAL>mfderiv I I' f x = f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>hxs : UniqueMDiffWithinAt I s x<GOAL>mfderivWithin I I' f s x = f'