ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>p q : ℚ<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedField K<GOAL>↑q ≤ 0 ↔ q ≤ 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝³ : Category.{?u.313, u_3} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>K L M : HomologicalComplex C c'<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>e : c.Embedding c'<VAR>inst✝ : e.IsRelIff<VAR>i j : ι<VAR>hij : ¬c.Rel i j<GOAL>¬c'.Rel (e.f i) (e.f j)
<VAR>m n : ℤ<VAR>k : ℕ<GOAL>(m.lor n).testBit k = (m.testBit k || n.testBit k)
<VAR>n : ℕ<GOAL>(n + 1).ascFactorial 0 ≤ (n + 0) ^ 0
<VAR>n k : ℕ<GOAL>(n + 1).ascFactorial (k + 1) ≤ (n + (k + 1)) ^ (k + 1)
<VAR>n k : ℕ<GOAL>(n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>one_le_n : 1 ≤ n<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>one_le_n : 1 ≤ n<VAR>p : TangentBundle I M<VAR>hp : p ∈ TotalSpace.proj ⁻¹' s<GOAL>∃ u, IsOpen u ∧ p ∈ u ∧ ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s ∩ u)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>one_le_n : 1 ≤ n<VAR>p : TangentBundle I M<VAR>hp : p ∈ TotalSpace.proj ⁻¹' s<VAR>hf' : ContinuousOn f s ∧ ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<GOAL>∃ u, IsOpen u ∧ p ∈ u ∧ ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s ∩ u)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>one_le_n : 1 ≤ n<VAR>p : TangentBundle I M<VAR>hf' : ContinuousOn f s ∧ ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hp : p.proj ∈ s<VAR>l : PartialHomeomorph M H := chartAt H p.proj<VAR>Dl : PartialHomeomorph (TangentBundle I M) (ModelProd H E) := chartAt (ModelProd H E) p<VAR>hDl : Dl = chartAt (ModelProd H E) p<VAR>r : PartialHomeomorph M' H' := chartAt H' (f p.proj)<VAR>Dr : PartialHomeomorph (TangentBundle I' M') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMapWithin I I' f s p)<VAR>il : PartialHomeomorph (TangentBundle I H) (ModelProd H E) := chartAt (ModelProd H E) (tangentMap I I (↑l) p)<VAR>ir : PartialHomeomorph (TangentBundle I' H') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMap I I' (↑r ∘ f) p)<VAR>s' : Set M := f ⁻¹' r.source ∩ s ∩ l.source<VAR>s'_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'<VAR>s'l : Set H := l.target ∩ ↑l.symm ⁻¹' s'<VAR>s'l_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'l<GOAL>∃ u, IsOpen u ∧ p ∈ u ∧ ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s ∩ u)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>one_le_n : 1 ≤ n<VAR>p : TangentBundle I M<VAR>hf' : ContinuousOn f s ∧ ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hp : p.proj ∈ s<VAR>l : PartialHomeomorph M H := chartAt H p.proj<VAR>Dl : PartialHomeomorph (TangentBundle I M) (ModelProd H E) := chartAt (ModelProd H E) p<VAR>hDl : Dl = chartAt (ModelProd H E) p<VAR>r : PartialHomeomorph M' H' := chartAt H' (f p.proj)<VAR>Dr : PartialHomeomorph (TangentBundle I' M') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMapWithin I I' f s p)<VAR>il : PartialHomeomorph (TangentBundle I H) (ModelProd H E) := chartAt (ModelProd H E) (tangentMap I I (↑l) p)<VAR>ir : PartialHomeomorph (TangentBundle I' H') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMap I I' (↑r ∘ f) p)<VAR>s' : Set M := f ⁻¹' r.source ∩ s ∩ l.source<VAR>s'_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'<VAR>s'l : Set H := l.target ∩ ↑l.symm ⁻¹' s'<VAR>s'l_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'l<VAR>o : Set M<VAR>o_open : IsOpen o<VAR>ho : f ⁻¹' r.source ∩ s = o ∩ s<GOAL>∃ u, IsOpen u ∧ p ∈ u ∧ ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s ∩ u)
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>one_le_n : 1 ≤ n<VAR>p : TangentBundle I M<VAR>hf' : ContinuousOn f s ∧ ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hp : p.proj ∈ s<VAR>l : PartialHomeomorph M H := chartAt H p.proj<VAR>Dl : PartialHomeomorph (TangentBundle I M) (ModelProd H E) := chartAt (ModelProd H E) p<VAR>hDl : Dl = chartAt (ModelProd H E) p<VAR>r : PartialHomeomorph M' H' := chartAt H' (f p.proj)<VAR>Dr : PartialHomeomorph (TangentBundle I' M') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMapWithin I I' f s p)<VAR>il : PartialHomeomorph (TangentBundle I H) (ModelProd H E) := chartAt (ModelProd H E) (tangentMap I I (↑l) p)<VAR>ir : PartialHomeomorph (TangentBundle I' H') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMap I I' (↑r ∘ f) p)<VAR>s' : Set M := f ⁻¹' r.source ∩ s ∩ l.source<VAR>s'_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'<VAR>s'l : Set H := l.target ∩ ↑l.symm ⁻¹' s'<VAR>s'l_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'l<VAR>o : Set M<VAR>o_open : IsOpen o<VAR>ho : f ⁻¹' r.source ∩ s = o ∩ s<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) s'_lift
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>one_le_n : 1 ≤ n<VAR>p : TangentBundle I M<VAR>hf' : ContinuousOn f s ∧ ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hp : p.proj ∈ s<VAR>l : PartialHomeomorph M H := chartAt H p.proj<VAR>Dl : PartialHomeomorph (TangentBundle I M) (ModelProd H E) := chartAt (ModelProd H E) p<VAR>hDl : Dl = chartAt (ModelProd H E) p<VAR>r : PartialHomeomorph M' H' := chartAt H' (f p.proj)<VAR>Dr : PartialHomeomorph (TangentBundle I' M') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMapWithin I I' f s p)<VAR>il : PartialHomeomorph (TangentBundle I H) (ModelProd H E) := chartAt (ModelProd H E) (tangentMap I I (↑l) p)<VAR>ir : PartialHomeomorph (TangentBundle I' H') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMap I I' (↑r ∘ f) p)<VAR>s' : Set M := f ⁻¹' r.source ∩ s ∩ l.source<VAR>s'_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'<VAR>s'l : Set H := l.target ∩ ↑l.symm ⁻¹' s'<VAR>s'l_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'l<VAR>o : Set M<VAR>o_open : IsOpen o<VAR>ho : f ⁻¹' r.source ∩ s = o ∩ s<VAR>U' : UniqueMDiffOn I s'<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) s'_lift
<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>Is : 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>I's : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹¹ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁰ : TopologicalSpace N<VAR>inst✝⁹ : ChartedSpace G N<VAR>Js : SmoothManifoldWithCorners J N<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>J's : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝³ : NormedAddCommGroup F₁<VAR>inst✝² : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝¹ : NormedAddCommGroup F₂<VAR>inst✝ : NormedSpace 𝕜 F₂<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hmn : m + 1 ≤ n<VAR>hs : UniqueMDiffOn I s<VAR>one_le_n : 1 ≤ n<VAR>p : TangentBundle I M<VAR>hf' : ContinuousOn f s ∧ ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))<VAR>hp : p.proj ∈ s<VAR>l : PartialHomeomorph M H := chartAt H p.proj<VAR>Dl : PartialHomeomorph (TangentBundle I M) (ModelProd H E) := chartAt (ModelProd H E) p<VAR>hDl : Dl = chartAt (ModelProd H E) p<VAR>r : PartialHomeomorph M' H' := chartAt H' (f p.proj)<VAR>Dr : PartialHomeomorph (TangentBundle I' M') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMapWithin I I' f s p)<VAR>il : PartialHomeomorph (TangentBundle I H) (ModelProd H E) := chartAt (ModelProd H E) (tangentMap I I (↑l) p)<VAR>ir : PartialHomeomorph (TangentBundle I' H') (ModelProd H' E') := chartAt (ModelProd H' E') (tangentMap I I' (↑r ∘ f) p)<VAR>s' : Set M := f ⁻¹' r.source ∩ s ∩ l.source<VAR>s'_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'<VAR>s'l : Set H := l.target ∩ ↑l.symm ⁻¹' s'<VAR>s'l_lift : Set (TotalSpace E (TangentSpace I)) := TotalSpace.proj ⁻¹' s'l<VAR>o : Set M<VAR>o_open : IsOpen o<VAR>ho : f ⁻¹' r.source ∩ s = o ∩ s<VAR>U' : UniqueMDiffOn I s'<VAR>U'l : UniqueMDiffOn I s'l<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) s'_lift