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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H 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>n : ℕ∞<VAR>hf : ContMDiff I' I n f<VAR>hg : ContMDiff I' I n g<GOAL>ContMDiff I' I n (f * g)
<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>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd 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>n : ℕ∞<VAR>hf : ContMDiff I' I n f<VAR>hg : ContMDiff I' I n g<GOAL>ContMDiff I' I n (f + g)
<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>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd 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>s : Set M<VAR>x : M<VAR>hf : SmoothWithinAt I' I f s x<VAR>hg : SmoothWithinAt I' I g s x<GOAL>SmoothWithinAt I' I (f + g) s x
<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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H 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>s : Set M<VAR>x : M<VAR>hf : SmoothWithinAt I' I f s x<VAR>hg : SmoothWithinAt I' I g s x<GOAL>SmoothWithinAt I' I (f * g) s x
<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>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd 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>x : M<VAR>hf : SmoothAt I' I f x<VAR>hg : SmoothAt I' I g x<GOAL>SmoothAt I' I (f + g) x
<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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H 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>x : M<VAR>hf : SmoothAt I' I f x<VAR>hg : SmoothAt I' I g x<GOAL>SmoothAt I' I (f * g) x
<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>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd 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>s : Set M<VAR>hf : SmoothOn I' I f s<VAR>hg : SmoothOn I' I g s<GOAL>SmoothOn I' I (f + g) s
<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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H 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>s : Set M<VAR>hf : SmoothOn I' I f s<VAR>hg : SmoothOn I' I g s<GOAL>SmoothOn I' I (f * g) s
<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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H 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<GOAL>Smooth I' I (f * g)
<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>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd 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<GOAL>Smooth I' I (f + g)
<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>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>a : G<GOAL>Smooth I I fun b => a + b
<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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>a : G<GOAL>Smooth I I fun b => a * b
<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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>a : G<GOAL>Smooth I I fun b => b * a
<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>Add G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>a : G<GOAL>Smooth I I fun b => b + a
<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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>g h : G<GOAL>(smoothLeftMul I g) h = g * h
<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>Mul G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>g h : G<GOAL>(smoothRightMul I g) h = h * g
<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_8<VAR>Semigroup G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>g h : G<GOAL>smoothLeftMul I (g * h) = (smoothLeftMul I g).comp (smoothLeftMul I h)
<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_8<VAR>Semigroup G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>g h : G<GOAL>smoothRightMul I (g * h) = (smoothRightMul I h).comp (smoothRightMul I g)
<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_8<VAR>Monoid G'<VAR>TopologicalSpace G'<VAR>ChartedSpace H G'<VAR>SmoothMul I G'<VAR>g' : G'<GOAL>(smoothLeftMul I g') 1 = g'
<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_8<VAR>Monoid G'<VAR>TopologicalSpace G'<VAR>ChartedSpace H G'<VAR>SmoothMul I G'<VAR>g' : G'<GOAL>(smoothRightMul I g') 1 = g'
<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>AddMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>n : ℕ<GOAL>Smooth I I fun a => n • a
<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>Monoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>n : ℕ<GOAL>Smooth I I fun a => a ^ n
<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>H' : Type u_5<VAR>TopologicalSpace H'<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>G : Type u_8<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddMonoid G<VAR>SmoothAdd I G<VAR>G' : Type u_9<VAR>TopologicalSpace G'<VAR>ChartedSpace H' G'<VAR>AddMonoid G'<VAR>SmoothAdd I' G'<VAR>self : SmoothAddMonoidMorphism I I' G G'<GOAL>Smooth I I' (↑self.toAddMonoidHom).toFun
<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>H' : Type u_5<VAR>TopologicalSpace H'<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>G : Type u_8<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Monoid G<VAR>SmoothMul I G<VAR>G' : Type u_9<VAR>TopologicalSpace G'<VAR>ChartedSpace H' G'<VAR>Monoid G'<VAR>SmoothMul I' G'<VAR>self : SmoothMonoidMorphism I I' G G'<GOAL>Smooth I I' (↑self.toMonoidHom).toFun
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => ∑ i ∈ t, f i x) s x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>lf : LocallyFinite fun i => Function.support (f i)<VAR>x₀ : M<VAR>h : ∀ (i : ι), ContMDiffWithinAt I' I n (f i) s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => ∑ᶠ (i : ι), f i x) s x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>lf : LocallyFinite fun i => Function.mulSupport (f i)<VAR>x₀ : M<VAR>h : ∀ (i : ι), ContMDiffWithinAt I' I n (f i) s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => ∏ᶠ (i : ι), f i x) s x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x<GOAL>ContMDiffWithinAt I' I n (∏ i ∈ t, f i) s x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x<GOAL>ContMDiffWithinAt I' I n (∑ i ∈ t, f i) s x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x<GOAL>ContMDiffWithinAt I' I n (fun x => ∑ i ∈ t, f i x) s x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x<GOAL>ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀<GOAL>ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀<GOAL>ContMDiffAt I' I n (fun x => ∑ i ∈ t, f i x) x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>x₀ : M<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>lf : LocallyFinite fun i => Function.support (f i)<VAR>h : ∀ (i : ι), ContMDiffAt I' I n (f i) x₀<GOAL>ContMDiffAt I' I n (fun x => ∑ᶠ (i : ι), f i x) x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>x₀ : M<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>lf : LocallyFinite fun i => Function.mulSupport (f i)<VAR>h : ∀ (i : ι), ContMDiffAt I' I n (f i) x₀<GOAL>ContMDiffAt I' I n (fun x => ∏ᶠ (i : ι), f i x) x₀
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x<GOAL>ContMDiffAt I' I n (∑ i ∈ t, f i) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x<GOAL>ContMDiffAt I' I n (∏ i ∈ t, f i) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x<GOAL>ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x<GOAL>ContMDiffAt I' I n (fun x => ∑ i ∈ t, f i x) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>lf : LocallyFinite fun i => Function.support (f i)<VAR>h : ∀ (i : ι), ContMDiffOn I' I n (f i) s<GOAL>ContMDiffOn I' I n (fun x => ∑ᶠ (i : ι), f i x) s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>lf : LocallyFinite fun i => Function.mulSupport (f i)<VAR>h : ∀ (i : ι), ContMDiffOn I' I n (f i) s<GOAL>ContMDiffOn I' I n (fun x => ∏ᶠ (i : ι), f i x) s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>AddCommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothAdd I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s<GOAL>ContMDiffOn I' I n (∑ i ∈ t, f i) s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>CommMonoid G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>SmoothMul I G<VAR>E' : Type u_6<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>TopologicalSpace M<VAR>ChartedSpace H' M<VAR>s : Set M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s<GOAL>ContMDiffOn I' I n (∏ i ∈ t, f i) s