ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>TopologicalSpace α<VAR>Zero α<VAR>T1Space α<VAR>f : G → α<VAR>hf : HasCompactSupport f<VAR>h'f : Continuous f<GOAL>f = 0 ∨ LocallyCompactSpace G
<VAR>G : Type w<VAR>α : Type u<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>TopologicalSpace α<VAR>Zero α<VAR>T1Space α<VAR>f : G → α<VAR>hf : HasCompactSupport f<VAR>h'f : Continuous f<GOAL>f = 0 ∨ LocallyCompactSpace G
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>LocallyCompactSpace G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 0<GOAL>∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 0 ∈ interior K
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>LocallyCompactSpace G<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<GOAL>∃ K, IsCompact K ∧ IsClosed K ∧ K ⊆ U ∧ 1 ∈ interior K
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>WeaklyLocallyCompactSpace G<GOAL>∃ K, IsCompact K ∧ IsClosed K ∧ K ∈ 𝓝 0
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>WeaklyLocallyCompactSpace G<GOAL>∃ K, IsCompact K ∧ IsClosed K ∧ K ∈ 𝓝 1
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x y : G<GOAL>𝓝 (x + y) = 𝓝 x + 𝓝 y
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x y : G<GOAL>𝓝 (x * y) = 𝓝 x * 𝓝 y
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>AddGroup G<VAR>TopologicalAddGroup G<VAR>x : G<GOAL>nhdsAddHom x = 𝓝 x
<VAR>G : Type w<VAR>TopologicalSpace G<VAR>Group G<VAR>TopologicalGroup G<VAR>x : G<GOAL>nhdsMulHom x = 𝓝 x
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousAdd G<VAR>Γ : AddSubgroup G<VAR>x : G ⧸ Γ<GOAL>Continuous fun g => g +ᵥ x
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousMul G<VAR>Γ : Subgroup G<VAR>x : G ⧸ Γ<GOAL>Continuous fun g => g • x
<VAR>G : Type w<VAR>Group G<VAR>TopologicalSpace G<VAR>ContinuousInv G<GOAL>Embedding Units.val
<VAR>G : Type w<VAR>AddGroup G<VAR>TopologicalSpace G<VAR>ContinuousNeg G<GOAL>Embedding AddUnits.val
<VAR>G : Type w<VAR>Group G<VAR>ts : Set (TopologicalSpace G)<VAR>h : ∀ t ∈ ts, TopologicalGroup G<GOAL>TopologicalGroup G
<VAR>G : Type w<VAR>AddGroup G<VAR>ts : Set (TopologicalSpace G)<VAR>h : ∀ t ∈ ts, TopologicalAddGroup G<GOAL>TopologicalAddGroup G
<VAR>G : Type w<VAR>ι : Sort u_1<VAR>Group G<VAR>ts' : ι → TopologicalSpace G<VAR>h' : ∀ (i : ι), TopologicalGroup G<GOAL>TopologicalGroup G
<VAR>G : Type w<VAR>ι : Sort u_1<VAR>AddGroup G<VAR>ts' : ι → TopologicalSpace G<VAR>h' : ∀ (i : ι), TopologicalAddGroup G<GOAL>TopologicalAddGroup G
<VAR>G : Type w<VAR>AddGroup G<VAR>t₁ t₂ : TopologicalSpace G<VAR>h₁ : TopologicalAddGroup G<VAR>h₂ : TopologicalAddGroup G<GOAL>TopologicalAddGroup G
<VAR>G : Type w<VAR>Group G<VAR>t₁ t₂ : TopologicalSpace G<VAR>h₁ : TopologicalGroup G<VAR>h₂ : TopologicalGroup G<GOAL>TopologicalGroup G
<VAR>α : Type u<VAR>Group α<VAR>g : GroupTopology α<GOAL>Continuous fun p => p.1 * p.2
<VAR>α : Type u<VAR>AddGroup α<VAR>g : AddGroupTopology α<GOAL>Continuous fun p => p.1 + p.2
<VAR>α : Type u<VAR>AddGroup α<VAR>g : AddGroupTopology α<GOAL>Continuous Neg.neg
<VAR>α : Type u<VAR>Group α<VAR>g : GroupTopology α<GOAL>Continuous Inv.inv
<VAR>α : Type u<VAR>Group α<GOAL>Function.Injective GroupTopology.toTopologicalSpace
<VAR>α : Type u<VAR>AddGroup α<GOAL>Function.Injective AddGroupTopology.toTopologicalSpace
<VAR>α : Type u<VAR>Group α<VAR>f g : GroupTopology α<VAR>h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen<GOAL>f = g
<VAR>α : Type u<VAR>AddGroup α<VAR>f g : AddGroupTopology α<VAR>h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen<GOAL>f = g
<VAR>α : Type u<VAR>Group α<VAR>x y : GroupTopology α<GOAL>x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y
<VAR>α : Type u<VAR>AddGroup α<VAR>x y : AddGroupTopology α<GOAL>x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y
<VAR>α : Type u<VAR>Group α<GOAL>⊤.toTopologicalSpace = ⊤
<VAR>α : Type u<VAR>AddGroup α<GOAL>⊤.toTopologicalSpace = ⊤
<VAR>α : Type u<VAR>Group α<GOAL>⊥.toTopologicalSpace = ⊥
<VAR>α : Type u<VAR>AddGroup α<GOAL>⊥.toTopologicalSpace = ⊥
<VAR>α : Type u<VAR>AddGroup α<VAR>x y : AddGroupTopology α<GOAL>(x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace
<VAR>α : Type u<VAR>Group α<VAR>x y : GroupTopology α<GOAL>(x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace
<VAR>α : Type u<VAR>Group α<VAR>s : Set (GroupTopology α)<GOAL>(sInf s).toTopologicalSpace = sInf (GroupTopology.toTopologicalSpace '' s)
<VAR>α : Type u<VAR>AddGroup α<VAR>s : Set (AddGroupTopology α)<GOAL>(sInf s).toTopologicalSpace = sInf (AddGroupTopology.toTopologicalSpace '' s)
<VAR>α : Type u<VAR>AddGroup α<VAR>ι : Sort u_1<VAR>s : ι → AddGroupTopology α<GOAL>(⨅ i, s i).toTopologicalSpace = ⨅ i, (s i).toTopologicalSpace
<VAR>α : Type u<VAR>Group α<VAR>ι : Sort u_1<VAR>s : ι → GroupTopology α<GOAL>(⨅ i, s i).toTopologicalSpace = ⨅ i, (s i).toTopologicalSpace
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>Group β<VAR>f : α → β<GOAL>Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>AddGroup β<VAR>f : α → β<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>self : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>ContMDiff I' I n ⇑self.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>self : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>ContMDiff I I' n ⇑self.toEquiv
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<GOAL>Function.Injective Diffeomorph.toEquiv
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>Continuous ⇑h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>ContMDiff I I' n ⇑h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<VAR>x : M<GOAL>ContMDiffAt I I' n (⇑h) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<VAR>s : Set M<VAR>x : M<GOAL>ContMDiffWithinAt I I' n (⇑h) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>n : ℕ∞<VAR>h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<GOAL>ContDiff 𝕜 n ⇑h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>h : M ≃ₘ⟮I, I'⟯ M'<GOAL>Smooth I I' ⇑h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<VAR>hn : 1 ≤ n<GOAL>MDifferentiable I I' ⇑h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<VAR>s : Set M<VAR>hn : 1 ≤ n<GOAL>MDifferentiableOn I I' (⇑h) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>⇑h.toEquiv = ⇑h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>⇑↑h = ⇑h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h h' : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>h.toEquiv = h'.toEquiv ↔ h = h'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<GOAL>Function.Injective DFunLike.coe
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h h' : M ≃ₘ^n⟮I, I'⟯ M'<VAR>Heq : ∀ (x : M), h x = h' x<GOAL>h = h'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>n : ℕ∞<GOAL>(Diffeomorph.refl I M n).toEquiv = Equiv.refl M
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>n : ℕ∞<GOAL>⇑(Diffeomorph.refl I M n) = id
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>h.trans (Diffeomorph.refl I' M' n) = h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, I'⟯ M'<GOAL>(Diffeomorph.refl I M n).trans h = h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h₁ : M ≃ₘ^n⟮I, I'⟯ M'<VAR>h₂ : M' ≃ₘ^n⟮I', J⟯ N<GOAL>⇑(h₁.trans h₂) = ⇑h₂ ∘ ⇑h₁
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>x : N<GOAL>h (h.symm x) = x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>x : M<GOAL>h.symm (h x) = x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>n : ℕ∞<GOAL>(Diffeomorph.refl I M n).symm = Diffeomorph.refl I M n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<GOAL>h.trans h.symm = Diffeomorph.refl I M n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<GOAL>h.symm.trans h = Diffeomorph.refl J N n
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>M' : Type u_10<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h₁ : M ≃ₘ^n⟮I, I'⟯ M'<VAR>h₂ : M' ≃ₘ^n⟮I', J⟯ N<GOAL>(h₁.trans h₂).symm = h₂.symm.trans h₁.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<GOAL>h.symm.toEquiv = h.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<GOAL>⇑h.symm = ⇑h.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>s : Set M<GOAL>⇑h '' s = ⇑h.symm ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>s : Set N<GOAL>⇑h.symm '' s = ⇑h ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>α : Sort u_13<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>f : α → M<GOAL>Set.range (⇑h ∘ f) = ⇑h.symm ⁻¹' Set.range f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>s : Set N<GOAL>⇑h '' (⇑h.symm '' s) = s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<VAR>s : Set M<GOAL>⇑h.symm '' (⇑h '' s) = s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<GOAL>h.toHomeomorph.toEquiv = h.toEquiv
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<GOAL>h.symm.toHomeomorph = h.toHomeomorph.symm
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<GOAL>⇑h.toHomeomorph = ⇑h
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>TopologicalSpace H<VAR>G : Type u_7<VAR>TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_9<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>N : Type u_11<VAR>TopologicalSpace N<VAR>ChartedSpace G N<VAR>n : ℕ∞<VAR>h : M ≃ₘ^n⟮I, J⟯ N<GOAL>⇑h.toHomeomorph.symm = ⇑h.symm