ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 (fun x => ∑ i ∈ t, 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>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s<GOAL>ContMDiffOn I' I n (fun x => ∏ i ∈ t, 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>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiff I' I n (f i)<GOAL>ContMDiff I' I n fun x => ∑ 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>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiff I' I n (f i)<GOAL>ContMDiff I' I n fun x => ∏ 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>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiff I' I n (f i)<GOAL>ContMDiff I' I n (∏ i ∈ t, f i)
<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>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ i ∈ t, ContMDiff I' I n (f i)<GOAL>ContMDiff I' I n (∑ i ∈ t, f i)
<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>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ (i : ι), ContMDiff I' I n (f i)<VAR>hfin : LocallyFinite fun i => Function.mulSupport (f i)<GOAL>ContMDiff I' I n fun x => ∏ᶠ (i : ι), 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>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>f : ι → M → G<VAR>n : ℕ∞<VAR>h : ∀ (i : ι), ContMDiff I' I n (f i)<VAR>hfin : LocallyFinite fun i => Function.support (f i)<GOAL>ContMDiff I' I n fun x => ∑ᶠ (i : ι), 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>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>f : ι → M → G<VAR>n : ℕ∞<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)<VAR>hf : LocallyFinite fun i => Function.support (f i)<GOAL>ContMDiff I' I n fun x => ∑ᶠ (i : ι) (_ : p i), 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>f : ι → M → G<VAR>n : ℕ∞<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)<VAR>hf : LocallyFinite fun i => Function.mulSupport (f i)<GOAL>ContMDiff I' I n fun x => ∏ᶠ (i : ι) (_ : p i), 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>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>lf : LocallyFinite fun i => Function.support (f i)<VAR>h : ∀ (i : ι), SmoothAt I' I (f i) x₀<GOAL>SmoothAt I' I (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>lf : LocallyFinite fun i => Function.mulSupport (f i)<VAR>h : ∀ (i : ι), SmoothAt I' I (f i) x₀<GOAL>SmoothAt I' I (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>s : Set M<VAR>x : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x<GOAL>SmoothWithinAt I' I (∏ 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>h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x<GOAL>SmoothWithinAt I' I (∑ 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>h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x<GOAL>SmoothWithinAt I' I (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>h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x<GOAL>SmoothWithinAt I' I (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>h : ∀ i ∈ t, SmoothAt I' I (f i) x<GOAL>SmoothAt I' I (∏ 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>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>h : ∀ i ∈ t, SmoothAt I' I (f i) x<GOAL>SmoothAt I' I (∑ 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>h : ∀ i ∈ t, SmoothAt I' I (f i) x<GOAL>SmoothAt I' I (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>h : ∀ i ∈ t, SmoothAt I' I (f i) x<GOAL>SmoothAt I' I (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>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>h : ∀ i ∈ t, SmoothOn I' I (f i) s<GOAL>SmoothOn I' I (∏ 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>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>h : ∀ i ∈ t, SmoothOn I' I (f i) s<GOAL>SmoothOn I' I (∑ 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>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>h : ∀ i ∈ t, SmoothOn I' I (f i) s<GOAL>SmoothOn I' I (fun x => ∑ i ∈ t, 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>t : Finset ι<VAR>f : ι → M → G<VAR>h : ∀ i ∈ t, SmoothOn I' I (f i) s<GOAL>SmoothOn I' I (fun x => ∏ i ∈ t, 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>t : Finset ι<VAR>f : ι → M → G<VAR>h : ∀ i ∈ t, Smooth I' I (f i)<GOAL>Smooth I' I (∑ i ∈ t, f i)
<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>t : Finset ι<VAR>f : ι → M → G<VAR>h : ∀ i ∈ t, Smooth I' I (f i)<GOAL>Smooth I' I (∏ i ∈ t, f i)
<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>t : Finset ι<VAR>f : ι → M → G<VAR>h : ∀ i ∈ t, Smooth I' I (f i)<GOAL>Smooth I' I fun x => ∏ 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>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>t : Finset ι<VAR>f : ι → M → G<VAR>h : ∀ i ∈ t, Smooth I' I (f i)<GOAL>Smooth I' I fun x => ∑ 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>f : ι → M → G<VAR>h : ∀ (i : ι), Smooth I' I (f i)<VAR>hfin : LocallyFinite fun i => Function.mulSupport (f i)<GOAL>Smooth I' I fun x => ∏ᶠ (i : ι), 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>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>f : ι → M → G<VAR>h : ∀ (i : ι), Smooth I' I (f i)<VAR>hfin : LocallyFinite fun i => Function.support (f i)<GOAL>Smooth I' I fun x => ∑ᶠ (i : ι), 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>f : ι → M → G<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → Smooth I' I (f i)<VAR>hf : LocallyFinite fun i => Function.mulSupport (f i)<GOAL>Smooth I' I fun x => ∏ᶠ (i : ι) (_ : p i), 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>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>f : ι → M → G<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → Smooth I' I (f i)<VAR>hf : LocallyFinite fun i => Function.support (f i)<GOAL>Smooth I' I fun x => ∑ᶠ (i : ι) (_ : p i), f i 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>DivInvMonoid 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 : M → G<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiffWithinAt I' I n f s x<GOAL>ContMDiffWithinAt I' I n (fun x => f x / c) 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>SubNegMonoid 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 : M → G<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiffWithinAt I' I n f s x<GOAL>ContMDiffWithinAt I' I n (fun x => f x - c) 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>DivInvMonoid 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 : M → G<VAR>x : M<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiffAt I' I n f x<GOAL>ContMDiffAt I' I n (fun x => f x / c) 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>SubNegMonoid 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 : M → G<VAR>x : M<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiffAt I' I n f x<GOAL>ContMDiffAt I' I n (fun x => f x - c) 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>SubNegMonoid 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 : M → G<VAR>s : Set M<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiffOn I' I n f s<GOAL>ContMDiffOn I' I n (fun x => f x - c) 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>DivInvMonoid 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 : M → G<VAR>s : Set M<VAR>n : ℕ∞<VAR>c : G<VAR>hf : ContMDiffOn I' I n f s<GOAL>ContMDiffOn I' I n (fun x => f x / c) s