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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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>x₀ : M<VAR>hf : SmoothAt I' I f x₀<GOAL>SmoothAt I' I (fun x => (f x)⁻¹) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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>x₀ : M<VAR>hf : SmoothAt I' I f x₀<GOAL>SmoothAt I' I (fun x => -f x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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>s : Set M<VAR>hf : SmoothOn I' I f s<GOAL>SmoothOn I' I (fun x => -f x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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>s : Set M<VAR>hf : SmoothOn I' I f s<GOAL>SmoothOn I' I (fun x => (f x)⁻¹) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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>hf : Smooth I' I f<GOAL>Smooth I' I fun x => -f 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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>hf : Smooth I' I f<GOAL>Smooth I' I fun x => (f 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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>n : ℕ∞<VAR>f g : M → G<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContMDiffWithinAt I' I n f s x₀<VAR>hg : ContMDiffWithinAt I' I n g s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => f x / g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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>n : ℕ∞<VAR>f g : M → G<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContMDiffWithinAt I' I n f s x₀<VAR>hg : ContMDiffWithinAt I' I n g s x₀<GOAL>ContMDiffWithinAt I' I n (fun x => f x - g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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>n : ℕ∞<VAR>f g : M → G<VAR>x₀ : M<VAR>hf : ContMDiffAt I' I n f x₀<VAR>hg : ContMDiffAt I' I n g x₀<GOAL>ContMDiffAt I' I n (fun x => f x / g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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>n : ℕ∞<VAR>f g : M → G<VAR>x₀ : M<VAR>hf : ContMDiffAt I' I n f x₀<VAR>hg : ContMDiffAt I' I n g x₀<GOAL>ContMDiffAt I' I n (fun x => f x - g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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>n : ℕ∞<VAR>f g : M → G<VAR>s : Set M<VAR>hf : ContMDiffOn I' I n f s<VAR>hg : ContMDiffOn I' I n g s<GOAL>ContMDiffOn I' I n (fun x => f x / g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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>n : ℕ∞<VAR>f g : M → G<VAR>s : Set M<VAR>hf : ContMDiffOn I' I n f s<VAR>hg : ContMDiffOn I' I n g s<GOAL>ContMDiffOn I' I n (fun x => f x - g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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>n : ℕ∞<VAR>f g : M → G<VAR>hf : ContMDiff I' I n f<VAR>hg : ContMDiff I' I n g<GOAL>ContMDiff I' I n fun x => f x / 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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>n : ℕ∞<VAR>f g : M → G<VAR>hf : ContMDiff I' I n f<VAR>hg : ContMDiff I' I n g<GOAL>ContMDiff I' I n fun x => f x - 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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 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 (fun x => f x - g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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 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 (fun x => f x / g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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 g : M → G<VAR>x₀ : M<VAR>hf : SmoothAt I' I f x₀<VAR>hg : SmoothAt I' I g x₀<GOAL>SmoothAt I' I (fun x => f x / g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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 g : M → G<VAR>x₀ : M<VAR>hf : SmoothAt I' I f x₀<VAR>hg : SmoothAt I' I g x₀<GOAL>SmoothAt I' I (fun x => f x - g x) 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Group G<VAR>LieGroup 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 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_5<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>AddGroup G<VAR>LieAddGroup 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 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>Inv G<VAR>Zero G<VAR>TopologicalSpace G<VAR>ChartedSpace H G<VAR>self : SmoothInv₀ I G<VAR>x : G<GOAL>x ≠ 0 → SmoothAt I I (fun y => y⁻¹) 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ I G<VAR>x : G<VAR>hx : x ≠ 0<GOAL>SmoothAt I I (fun y => y⁻¹) 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ I G<GOAL>HasContinuousInv₀ 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ I G<GOAL>SmoothOn I I Inv.inv {0}ᶜ
<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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ 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>n : ℕ∞<VAR>f : M → G<VAR>s : Set M<VAR>a : M<VAR>hf : ContMDiffWithinAt I' I n f s a<VAR>ha : f a ≠ 0<GOAL>ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ 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>n : ℕ∞<VAR>f : M → G<VAR>a : M<VAR>hf : ContMDiffAt I' I n f a<VAR>ha : f a ≠ 0<GOAL>ContMDiffAt I' I n (fun x => (f x)⁻¹) 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ 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>n : ℕ∞<VAR>f : M → G<VAR>hf : ContMDiff I' I n f<VAR>h0 : ∀ (x : M), f x ≠ 0<GOAL>ContMDiff I' I n fun x => (f 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ 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>n : ℕ∞<VAR>f : M → G<VAR>s : Set M<VAR>hf : ContMDiffOn I' I n f s<VAR>h0 : ∀ x ∈ s, f x ≠ 0<GOAL>ContMDiffOn I' I n (fun x => (f x)⁻¹) 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ 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>a : M<VAR>hf : SmoothWithinAt I' I f s a<VAR>ha : f a ≠ 0<GOAL>SmoothWithinAt I' I (fun x => (f x)⁻¹) s 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ 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>a : M<VAR>hf : SmoothAt I' I f a<VAR>ha : f a ≠ 0<GOAL>SmoothAt I' I (fun x => (f x)⁻¹) 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ 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>hf : Smooth I' I f<VAR>h0 : ∀ (x : M), f x ≠ 0<GOAL>Smooth I' I fun x => (f 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>Inv G<VAR>Zero G<VAR>SmoothInv₀ 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>hf : SmoothOn I' I f s<VAR>h0 : ∀ x ∈ s, f x ≠ 0<GOAL>SmoothOn I' I (fun x => (f x)⁻¹) 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>GroupWithZero G<VAR>SmoothInv₀ I 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>a : M<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I' I n f s a<VAR>hg : ContMDiffWithinAt I' I n g s a<VAR>h₀ : g a ≠ 0<GOAL>ContMDiffWithinAt I' I n (f / g) s 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>GroupWithZero G<VAR>SmoothInv₀ I 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>n : ℕ∞<VAR>hf : ContMDiffOn I' I n f s<VAR>hg : ContMDiffOn I' I n g s<VAR>h₀ : ∀ x ∈ s, g x ≠ 0<GOAL>ContMDiffOn I' I n (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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>GroupWithZero G<VAR>SmoothInv₀ I 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>a : M<VAR>n : ℕ∞<VAR>hf : ContMDiffAt I' I n f a<VAR>hg : ContMDiffAt I' I n g a<VAR>h₀ : g a ≠ 0<GOAL>ContMDiffAt I' I n (f / g) 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>GroupWithZero G<VAR>SmoothInv₀ I 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<VAR>h₀ : ∀ (x : M), g x ≠ 0<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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>GroupWithZero G<VAR>SmoothInv₀ I 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>a : M<VAR>hf : SmoothWithinAt I' I f s a<VAR>hg : SmoothWithinAt I' I g s a<VAR>h₀ : g a ≠ 0<GOAL>SmoothWithinAt I' I (f / g) s 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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>GroupWithZero G<VAR>SmoothInv₀ I 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<VAR>h₀ : ∀ x ∈ s, g x ≠ 0<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>TopologicalSpace G<VAR>ChartedSpace H G<VAR>GroupWithZero G<VAR>SmoothInv₀ I 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>a : M<VAR>hf : SmoothAt I' I f a<VAR>hg : SmoothAt I' I g a<VAR>h₀ : g a ≠ 0<GOAL>SmoothAt I' I (f / g) a