<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<VAR>diff_irrfl_lift : ContMDiffOn I.tangent I'.tangent m (↑ir ∘ tangentMapWithin I I' (↑r ∘ f ∘ ↑l.symm) s'l) s'l_lift<VAR>diff_Drirrfl_lift : ContMDiffOn I.tangent I'.tangent m (↑Dr.symm ∘ ↑ir ∘ tangentMapWithin I I' (↑r ∘ f ∘ ↑l.symm) s'l) s'l_lift<VAR>diff_DrirrflilDl : ContMDiffOn I.tangent I'.tangent m (↑Dr.symm ∘ (↑ir ∘ tangentMapWithin I I' (↑r ∘ f ∘ ↑l.symm) s'l) ∘ ↑il.symm ∘ ↑Dl) s'_lift<VAR>eq_comp : ∀ q ∈ s'_lift, tangentMapWithin I I' f s q = (↑Dr.symm ∘ ↑ir ∘ tangentMapWithin I I' (↑r ∘ f ∘ ↑l.symm) s'l ∘ ↑il.symm ∘ ↑Dl) q<GOAL>ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s) s'_lift