ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<VAR>diff_f : ContMDiffOn I I' n f 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<VAR>diff_f : ContMDiffOn I I' n f s'<VAR>diff_r : ContMDiffOn I' I' n (↑r) r.source<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<VAR>diff_f : ContMDiffOn I I' n f s'<VAR>diff_r : ContMDiffOn I' I' n (↑r) r.source<VAR>diff_rf : ContMDiffOn I I' n (↑r ∘ f) 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<VAR>diff_f : ContMDiffOn I I' n f s'<VAR>diff_r : ContMDiffOn I' I' n (↑r) r.source<VAR>diff_rf : ContMDiffOn I I' n (↑r ∘ f) s'<VAR>diff_l : ContMDiffOn I I n (↑l.symm) s'l<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<VAR>diff_f : ContMDiffOn I I' n f s'<VAR>diff_r : ContMDiffOn I' I' n (↑r) r.source<VAR>diff_rf : ContMDiffOn I I' n (↑r ∘ f) s'<VAR>diff_l : ContMDiffOn I I n (↑l.symm) s'l<VAR>diff_rfl : ContMDiffOn I I' n (↑r ∘ f ∘ ↑l.symm) s'l<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<VAR>diff_f : ContMDiffOn I I' n f s'<VAR>diff_r : ContMDiffOn I' I' n (↑r) r.source<VAR>diff_rf : ContMDiffOn I I' n (↑r ∘ f) s'<VAR>diff_l : ContMDiffOn I I n (↑l.symm) s'l<VAR>diff_rfl : ContMDiffOn I I' n (↑r ∘ f ∘ ↑l.symm) s'l<VAR>diff_rfl_lift : ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' (↑r ∘ f ∘ ↑l.symm) s'l) s'l_lift<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) s'_lift
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b c : α<VAR>h : IsUnit b<VAR>a : α<GOAL>a / b * b = a
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x₁ y₁ x₂ y₂ : α<GOAL>dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x₁ y₁ x₂ y₂ : α<GOAL>dist x₁ y₁ ≤ dist x₁ x₂ + dist x₂ y₂ + dist y₂ y₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>t₂.orthocenter = t₁.points i₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>t₁.points i₁ ∈ altitude t₂ j₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>t₁.points i₁ ∈ altitude t₂ j₃
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ≥0<VAR>hfi : Integrable (fun x => ↑(f x)) μ<VAR>b : ℝ≥0<GOAL>∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b ↔ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c c' : Cardinal.{u_3}<VAR>h : c.ord = c'.ord<GOAL>c = c'
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l (𝓝 C)<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Tendsto f l atTop<VAR>hg : Tendsto g l (𝓝 C)<VAR>this : Tendsto (fun x => f x * -g x) l atTop<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n✝ : σ →₀ ℕ<VAR>φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R<VAR>n : σ →₀ ℕ<GOAL>(coeff R n) (φ₁ * (φ₂ + φ₃)) = (coeff R n) (φ₁ * φ₂ + φ₁ * φ₃)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>hsc : sᶜ ∉ f<VAR>h : ↑f ⊓ 𝓟 s = ⊥<GOAL>↑f ⊓ 𝓟 sᶜᶜ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)<GOAL>∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : OpensMeasurableSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : OpensMeasurableSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : TopologicalSpace γ₂<VAR>inst✝² : MeasurableSpace γ₂<VAR>inst✝¹ : BorelSpace γ₂<VAR>inst✝ : MeasurableSpace δ<VAR>f : δ → γ<VAR>hf : ∀ (s : Set γ), IsClosed s → MeasurableSet (f ⁻¹' s)<VAR>s : Set γ<VAR>hs : IsOpen s<GOAL>MeasurableSet (f ⁻¹' s)