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>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>x : M<VAR>f : M → M'<VAR>g : M → M''<VAR>hf : MDifferentiableAt I I' f x<VAR>hg : MDifferentiableAt I I'' g x<GOAL>MDifferentiableAt I (I'.prod I'') (fun x => (f x, g 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>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>s : Set M<VAR>f : M → M'<VAR>g : M → M''<VAR>hf : MDifferentiableOn I I' f s<VAR>hg : MDifferentiableOn I I'' g s<GOAL>MDifferentiableOn I (I'.prod I'') (fun x => (f x, g x)) 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>g : M → M''<VAR>hf : MDifferentiable I I' f<VAR>hg : MDifferentiable I I'' g<GOAL>MDifferentiable I (I'.prod I'') fun x => (f x, g 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>x : M<VAR>s : Set M<VAR>f : M → E'<VAR>g : M → E''<VAR>hf : MDifferentiableWithinAt I 𝓘(𝕜, E') f s x<VAR>hg : MDifferentiableWithinAt I 𝓘(𝕜, E'') g s x<GOAL>MDifferentiableWithinAt I 𝓘(𝕜, E' × E'') (fun x => (f x, g x)) 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>x : M<VAR>f : M → E'<VAR>g : M → E''<VAR>hf : MDifferentiableAt I 𝓘(𝕜, E') f x<VAR>hg : MDifferentiableAt I 𝓘(𝕜, E'') g x<GOAL>MDifferentiableAt I 𝓘(𝕜, E' × E'') (fun x => (f x, g 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>s : Set M<VAR>f : M → E'<VAR>g : M → E''<VAR>hf : MDifferentiableOn I 𝓘(𝕜, E') f s<VAR>hg : MDifferentiableOn I 𝓘(𝕜, E'') g s<GOAL>MDifferentiableOn I 𝓘(𝕜, E' × E'') (fun x => (f x, g x)) 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>E'' : Type u_8<VAR>NormedAddCommGroup E''<VAR>NormedSpace 𝕜 E''<VAR>f : M → E'<VAR>g : M → E''<VAR>hf : MDifferentiable I 𝓘(𝕜, E') f<VAR>hg : MDifferentiable I 𝓘(𝕜, E'') g<GOAL>MDifferentiable I 𝓘(𝕜, E' × E'') fun x => (f x, g 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' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivAt I I' f x f'<VAR>h' : f' = f₁'<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>f' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>h' : f' = 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 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>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<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 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 : ∀ x ∈ t, f₁ x = f x<VAR>hx : f₁ x = f x<VAR>h₁ : t ⊆ s<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 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'<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<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 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<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<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 f₁ : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>MDifferentiableWithinAt I I' f s x ↔ 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 f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : MDifferentiableWithinAt I I' f s x<VAR>ht : ∀ x ∈ t, f₁ x = f x<VAR>hx : f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>MDifferentiableWithinAt I I' f₁ 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>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 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<VAR>ht : ∀ x ∈ s, f₁ x = f x<VAR>hx : f₁ x = f x<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 f₁ : M → M'<VAR>s t : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : MDifferentiableOn I I' f s<VAR>h' : ∀ x ∈ t, f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>MDifferentiableOn I I' f₁ 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 f₁ : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : MDifferentiableAt I I' f x<VAR>hL : 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 f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : MDifferentiableWithinAt I I' f s x<VAR>hs : ∀ x ∈ t, f₁ x = f x<VAR>hx : f₁ x = f x<VAR>hxt : UniqueMDiffWithinAt I t x<VAR>h₁ : t ⊆ s<GOAL>mfderivWithin I I' f₁ t 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 f₁ : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>hs : UniqueMDiffWithinAt I s x<VAR>hL : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>mfderivWithin 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 f₁ : M → M'<VAR>x : M<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>hs : UniqueMDiffWithinAt I s x<VAR>hL : ∀ x ∈ s, f₁ x = f x<VAR>hx : f₁ x = f x<GOAL>mfderivWithin 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 f₁ : M → M'<VAR>s : Set M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>h : ∀ x ∈ s, f x = f₁ x<VAR>p : TangentBundle I M<VAR>hp : p.proj ∈ s<VAR>hs : UniqueMDiffWithinAt I s p.proj<GOAL>tangentMapWithin I I' f s p = tangentMapWithin I I' f₁ s 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>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 f₁ : M → M'<VAR>x : M<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>mfderiv 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>x' : M<VAR>h : x = x'<GOAL>mfderiv 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>f' : M → M'<VAR>h : f = f'<GOAL>mfderiv 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>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>x : M<VAR>s : Set M<VAR>g : M' → M''<VAR>h : ContinuousWithinAt f s x<GOAL>{y | writtenInExtChartAt I I'' x (g ∘ f) y = (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) y} ∈ 𝓝[↑(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>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>x : M<VAR>s : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>hg : HasMFDerivWithinAt I' I'' g u (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hst : s ⊆ f ⁻¹' u<GOAL>HasMFDerivWithinAt I I'' (g ∘ f) s x (g'.comp 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>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>x : M<VAR>g : M' → M''<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>hg : HasMFDerivAt I' I'' g (f x) g'<VAR>hf : HasMFDerivAt I I' f x f'<GOAL>HasMFDerivAt I I'' (g ∘ f) x (g'.comp 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>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>x : M<VAR>s : Set M<VAR>g : M' → M''<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>hg : HasMFDerivAt I' I'' g (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<GOAL>HasMFDerivWithinAt I I'' (g ∘ f) s x (g'.comp 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>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>x : M<VAR>s : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>hg : MDifferentiableWithinAt I' I'' g u (f x)<VAR>hf : MDifferentiableWithinAt I I' f s x<VAR>h : s ⊆ f ⁻¹' u<GOAL>MDifferentiableWithinAt 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>x : M<VAR>g : M' → M''<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>hg : MDifferentiableAt I' I'' g (f x)<VAR>hf : MDifferentiableAt I I' f x<GOAL>MDifferentiableAt I I'' (g ∘ f) x