ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : Module 𝕜 E<VAR>inst✝¹² : TopologicalSpace E<VAR>inst✝¹¹ : TopologicalAddGroup E<VAR>inst✝¹⁰ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalAddGroup F<VAR>inst✝⁵ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁴ : AddCommGroup F'<VAR>inst✝³ : Module 𝕜 F'<VAR>inst✝² : TopologicalSpace F'<VAR>inst✝¹ : TopologicalAddGroup F'<VAR>inst✝ : ContinuousSMul 𝕜 F'<VAR>t : TopologicalSpace 𝕜<VAR>h₁ : TopologicalAddGroup 𝕜<VAR>h₂ : ContinuousSMul 𝕜 𝕜<VAR>h₃ : T2Space 𝕜<GOAL>t = UniformSpace.toTopologicalSpace
<VAR>𝕜 : Type u<VAR>hnorm : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : Module 𝕜 E<VAR>inst✝¹² : TopologicalSpace E<VAR>inst✝¹¹ : TopologicalAddGroup E<VAR>inst✝¹⁰ : ContinuousSMul 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module 𝕜 F<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalAddGroup F<VAR>inst✝⁵ : ContinuousSMul 𝕜 F<VAR>F' : Type x<VAR>inst✝⁴ : AddCommGroup F'<VAR>inst✝³ : Module 𝕜 F'<VAR>inst✝² : TopologicalSpace F'<VAR>inst✝¹ : TopologicalAddGroup F'<VAR>inst✝ : ContinuousSMul 𝕜 F'<VAR>t : TopologicalSpace 𝕜<VAR>h₁ : TopologicalAddGroup 𝕜<VAR>h₂ : ContinuousSMul 𝕜 𝕜<VAR>h₃ : T2Space 𝕜<GOAL>nhds 0 ≤ nhds 0
<VAR>m n✝ a✝ b✝ c✝ d a b n c : ℤ<VAR>ha : a ≡ b [ZMOD n]<GOAL>a - n * c ≡ b [ZMOD n]
<VAR>m n✝ a✝ b✝ c✝ d a b n c : ℤ<VAR>ha : a ≡ b [ZMOD n]<GOAL>a - n * c = a + n * -c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<GOAL>essSup f (μ.restrict s) = essSup f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<GOAL>essSup f μ ≤ essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<GOAL>c < essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<VAR>d : ℝ≥0∞<VAR>cd : c < d<VAR>hd : d < essSup f μ<GOAL>c < essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<VAR>d : ℝ≥0∞<VAR>cd : c < d<VAR>hd : d < essSup f μ<VAR>t : Set α := {x | d < f x}<GOAL>c < essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<VAR>d : ℝ≥0∞<VAR>cd : c < d<VAR>hd : d < essSup f μ<VAR>t : Set α := {x | d < f x}<VAR>A : 0 < (μ.restrict t) t<GOAL>c < essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<VAR>d : ℝ≥0∞<VAR>cd : c < d<VAR>hd : d < essSup f μ<VAR>t : Set α := {x | d < f x}<VAR>A : 0 < (μ.restrict t) t<VAR>B : 0 < (μ.restrict s) t<GOAL>c < essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<VAR>d : ℝ≥0∞<VAR>cd : c < d<VAR>hd : d < essSup f μ<VAR>t : Set α := {x | d < f x}<VAR>A : 0 < (μ.restrict t) t<VAR>B : 0 < (μ.restrict s) t<GOAL>d ≤ essSup f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<VAR>d : ℝ≥0∞<VAR>cd : c < d<VAR>hd : d < essSup f μ<VAR>t : Set α := {x | d < f x}<VAR>A : 0 < (μ.restrict t) t<VAR>B : 0 < (μ.restrict s) t<GOAL>d ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<VAR>d : ℝ≥0∞<VAR>cd : c < d<VAR>hd : d < essSup f μ<VAR>t : Set α := {x | d < f x}<VAR>A : 0 < (μ.restrict t) t<VAR>B : 0 < (μ.restrict s) t<VAR>b : ℝ≥0∞<VAR>hb : b ∈ {a | (μ.restrict s) {x | a < f x} = 0}<GOAL>d ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f✝ : α → ℝ≥0∞<VAR>s : Set α<VAR>f : α → ℝ≥0∞<VAR>hsf : Function.support f ⊆ s<VAR>c : ℝ≥0∞<VAR>hc : c < essSup f μ<VAR>d : ℝ≥0∞<VAR>cd : c < d<VAR>hd : d < essSup f μ<VAR>t : Set α := {x | d < f x}<VAR>A : 0 < (μ.restrict t) t<VAR>B : 0 < (μ.restrict s) t<VAR>b : ℝ≥0∞<VAR>hb : b < d<GOAL>b ∉ {a | (μ.restrict s) {x | a < f x} = 0}
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝ : Infinite α<VAR>s : Set α<VAR>hs : s.Finite<VAR>h : sᶜ.Finite<GOAL>univ.Finite
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>evenKernel a x = 0
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<VAR>this : (I * ↑x).im ≤ 0<GOAL>evenKernel a x = 0
<VAR>x : ℝ<VAR>hx : x ≤ 0<VAR>this : (I * ↑x).im ≤ 0<VAR>a' : ℝ<GOAL>evenKernel (↑a') x = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<VAR>inst✝¹ : SeparableSpace α<VAR>inst✝ : Nonempty α<GOAL>∃ u, DenseRange u
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>inst✝¹ : SeparableSpace α<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>hs : s.Countable<VAR>s_dense : Dense s<GOAL>∃ u, DenseRange u
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>inst✝¹ : SeparableSpace α<VAR>inst✝ : Nonempty α<VAR>s : Set α<VAR>hs : s.Countable<VAR>s_dense : Dense s<VAR>u : ℕ → α<VAR>hu : s ⊆ range u<GOAL>∃ u, DenseRange u
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<GOAL>cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<VAR>h : cons y s ≠ 0<GOAL>y ≠ 0 ∨ s ≠ 0
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<VAR>h : cons y s ≠ 0<VAR>h' : y = 0<VAR>c : s = 0<GOAL>cons y s = 0
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist (closure s) t = hausdorffEdist s t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist (closure s) t ≤ hausdorffEdist s t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist s t ≤ hausdorffEdist (closure s) t
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i✝ j✝ k✝ : J<VAR>s : Set (F.obj i✝)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>i j : J<VAR>f g : i ⟶ j<VAR>k : J<VAR>φ : k ⟶ i<VAR>hφ : φ ≫ f = φ ≫ g<GOAL>(fun g => g ∘ F.map φ) (F.map f) = (fun g => g ∘ F.map φ) (F.map g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>S : Set (Set α)<VAR>hc : S.Countable<VAR>hμ : ∀ s ∈ S, μ s < ⊤<VAR>hU : ⋃₀ S = univ<GOAL>SigmaFinite μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>S : Set (Set α)<VAR>hc : S.Countable<VAR>hμ✝ : ∀ s ∈ S, μ s < ⊤<VAR>hU : ⋃₀ S = univ<VAR>s : ℕ → Set α<VAR>hμ : ∀ (n : ℕ), μ (s n) < ⊤<VAR>hs : ⋃ n, s n = univ<GOAL>SigmaFinite μ
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>α : ↥H → K<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>h : ↥H<GOAL>⁅h, x⁆ = α h • x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>α : ↥H → K<VAR>x : L<VAR>h : ↥H<VAR>hx : x ∈ ((ad K L) ↑h).maxGenEigenspace (α h)<GOAL>⁅h, x⁆ = α h • x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>α : ↥H → K<VAR>x : L<VAR>h : ↥H<VAR>hx : ((ad K L) ↑h) x = α h • x<GOAL>⁅h, x⁆ = α h • x
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>hb : 1 < b<GOAL>a < b ^ a
<VAR>α β : Type u<VAR>a b : Cardinal.{u_1}<VAR>hb : 2 ≤ b<GOAL>a < b ^ a
<VAR>F : Type u_1<VAR>K✝¹ : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K✝¹<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F K✝¹<VAR>inst✝¹ : Algebra F L<VAR>K✝ K' : IntermediateField F L<VAR>inst✝ : Normal F L<VAR>K : IntermediateField F L<GOAL>Normal F ↥K ↔ ∀ (σ : L →ₐ[F] L), map σ K ≤ K
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<GOAL>ContDiffWithinAtProp I I' n f s x ↔ ContDiffWithinAtProp I I' n f (s ∩ u) x
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u<GOAL>ContDiffWithinAtProp I I' n f s x ↔ ContDiffWithinAtProp I I' n f (s ∩ u) x
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u<GOAL>ContDiffWithinAt 𝕜 n (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u) (↑I x) ↔ ContDiffWithinAt 𝕜 n (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>this : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u<GOAL>↑I.symm ⁻¹' u ∈ 𝓝 (↑I x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<VAR>u_open : IsOpen u<VAR>xu : x ∈ u<VAR>this✝ : ↑I.symm ⁻¹' (s ∩ u) ∩ range ↑I = ↑I.symm ⁻¹' s ∩ range ↑I ∩ ↑I.symm ⁻¹' u<VAR>this : u ∈ 𝓝 (↑I.symm (↑I x))<GOAL>↑I.symm ⁻¹' u ∈ 𝓝 (↑I x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e✝ : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ contDiffGroupoid ⊤ I<VAR>hx : x ∈ e.source<VAR>h : ContDiffWithinAt 𝕜 n (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) ((↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x)))<VAR>this✝ : ↑I x = (↑I ∘ ↑e.symm ∘ ↑I.symm) (↑I (↑e x))<VAR>this : ↑I (↑e x) ∈ ↑I.symm ⁻¹' e.target ∩ range ↑I<GOAL>ContDiffWithinAt 𝕜 n (↑I' ∘ (f ∘ ↑e.symm) ∘ ↑I.symm) (↑I.symm ⁻¹' (↑e.symm ⁻¹' s) ∩ range ↑I) (↑I (↑e x))