From 147826d8243539e805a2f46a2be65a1d7fbc999e Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sun, 28 Feb 2021 22:54:58 +0000
Subject: [PATCH] feat(geometry/manifold): `ext_chart_at` is smooth on its
 source (#6473)

---
 src/analysis/calculus/times_cont_diff.lean    |  5 ++
 .../smooth_manifold_with_corners.lean         | 79 ++++++++++++-------
 src/geometry/manifold/times_cont_mdiff.lean   | 40 ++++++++++
 3 files changed, 94 insertions(+), 30 deletions(-)

diff --git a/src/analysis/calculus/times_cont_diff.lean b/src/analysis/calculus/times_cont_diff.lean
index 03b41bb7d6dcb..3f53f9b812b40 100644
--- a/src/analysis/calculus/times_cont_diff.lean
+++ b/src/analysis/calculus/times_cont_diff.lean
@@ -467,6 +467,11 @@ lemma times_cont_diff_within_at.congr {n : with_top ℕ}
   times_cont_diff_within_at 𝕜 n f₁ s x :=
 h.congr_of_eventually_eq (filter.eventually_eq_of_mem self_mem_nhds_within h₁) hx
 
+lemma times_cont_diff_within_at.congr' {n : with_top ℕ}
+  (h : times_cont_diff_within_at 𝕜 n f s x) (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : x ∈ s) :
+  times_cont_diff_within_at 𝕜 n f₁ s x :=
+h.congr h₁ (h₁ _ hx)
+
 lemma times_cont_diff_within_at.mono_of_mem {n : with_top ℕ}
   (h : times_cont_diff_within_at 𝕜 n f s x) {t : set E} (hst : s ∈ 𝓝[t] x) :
   times_cont_diff_within_at 𝕜 n f t x :=
diff --git a/src/geometry/manifold/smooth_manifold_with_corners.lean b/src/geometry/manifold/smooth_manifold_with_corners.lean
index 0cf4354e8dd82..b5d42b1ae5088 100644
--- a/src/geometry/manifold/smooth_manifold_with_corners.lean
+++ b/src/geometry/manifold/smooth_manifold_with_corners.lean
@@ -633,6 +633,11 @@ of `x` to the model vector space. -/
 @[simp, mfld_simps] def ext_chart_at (x : M) : local_equiv M E :=
 (chart_at H x).to_local_equiv.trans I.to_local_equiv
 
+lemma ext_chart_at_coe : ⇑(ext_chart_at I x) = I ∘ chart_at H x := rfl
+
+lemma ext_chart_at_coe_symm :
+  ⇑(ext_chart_at I x).symm = (chart_at H x).symm ∘ I.symm := rfl
+
 lemma ext_chart_at_source : (ext_chart_at I x).source = (chart_at H x).source :=
 by rw [ext_chart_at, local_equiv.trans_source, I.source_eq, preimage_univ, inter_univ]
 
@@ -646,21 +651,27 @@ lemma ext_chart_at_to_inv :
   (ext_chart_at I x).symm ((ext_chart_at I x) x) = x :=
 by simp only with mfld_simps
 
+lemma ext_chart_at_source_mem_nhds' {x' : M} (h : x' ∈ (ext_chart_at I x).source) :
+  (ext_chart_at I x).source ∈ 𝓝 x' :=
+mem_nhds_sets (ext_chart_at_open_source I x) h
+
 lemma ext_chart_at_source_mem_nhds : (ext_chart_at I x).source ∈ 𝓝 x :=
-mem_nhds_sets (ext_chart_at_open_source I x) (mem_ext_chart_source I x)
+ext_chart_at_source_mem_nhds' I x (mem_ext_chart_source I x)
 
 lemma ext_chart_at_continuous_on :
   continuous_on (ext_chart_at I x) (ext_chart_at I x).source :=
 begin
-  refine continuous_on.comp I.continuous.continuous_on _ subset_preimage_univ,
+  refine I.continuous.comp_continuous_on _,
   rw ext_chart_at_source,
   exact (chart_at H x).continuous_on
 end
 
-lemma ext_chart_at_continuous_at :
-  continuous_at (ext_chart_at I x) x :=
-(ext_chart_at_continuous_on I x x (mem_ext_chart_source I x)).continuous_at
-  (ext_chart_at_source_mem_nhds I x)
+lemma ext_chart_at_continuous_at' {x' : M} (h : x' ∈ (ext_chart_at I x).source) :
+  continuous_at (ext_chart_at I x) x' :=
+(ext_chart_at_continuous_on I x).continuous_at $ ext_chart_at_source_mem_nhds' I x h
+
+lemma ext_chart_at_continuous_at : continuous_at (ext_chart_at I x) x :=
+ext_chart_at_continuous_at' _ _ (mem_ext_chart_source I x)
 
 lemma ext_chart_at_continuous_on_symm :
   continuous_on (ext_chart_at I x).symm (ext_chart_at I x).target :=
@@ -669,48 +680,56 @@ begin
   simp [ext_chart_at, local_equiv.trans_target]
 end
 
-lemma ext_chart_at_target_mem_nhds_within :
-  (ext_chart_at I x).target ∈ 𝓝[range I] ((ext_chart_at I x) x) :=
+lemma ext_chart_at_map_nhds' {x y : M} (hy : y ∈ (ext_chart_at I x).source) :
+  map (ext_chart_at I x) (𝓝 y) = 𝓝[range I] (ext_chart_at I x y) :=
 begin
-  rw [ext_chart_at, local_equiv.trans_target],
-  simp only [function.comp_app, local_equiv.coe_trans, model_with_corners.target_eq],
-  refine inter_mem_nhds_within _
-    (mem_nhds_sets ((chart_at H x).open_target.preimage I.continuous_symm) _),
-  simp only with mfld_simps
+  rw [ext_chart_at_coe, (∘), ← I.map_nhds_eq, ← (chart_at H x).map_nhds_eq, map_map],
+  rwa ext_chart_at_source at hy
 end
 
-lemma ext_chart_at_coe (p : M) : (ext_chart_at I x) p = I ((chart_at H x : M → H) p) := rfl
+lemma ext_chart_at_map_nhds :
+  map (ext_chart_at I x) (𝓝 x) = 𝓝[range I] (ext_chart_at I x x) :=
+ext_chart_at_map_nhds' I $ mem_ext_chart_source I x
+
+lemma ext_chart_at_target_mem_nhds_within :
+  (ext_chart_at I x).target ∈ 𝓝[range I] (ext_chart_at I x x) :=
+begin
+  rw [← local_equiv.image_source_eq_target, ← ext_chart_at_map_nhds],
+  exact image_mem_map (ext_chart_at_source_mem_nhds _ _)
+end
 
-lemma ext_chart_at_coe_symm (p : E) :
-  (ext_chart_at I x).symm p = ((chart_at H x).symm : H → M) (I.symm p) := rfl
+lemma ext_chart_at_target_subset_range : (ext_chart_at I x).target ⊆ range I :=
+by simp only with mfld_simps
 
 lemma nhds_within_ext_chart_target_eq :
   𝓝[(ext_chart_at I x).target] ((ext_chart_at I x) x) =
   𝓝[range I] ((ext_chart_at I x) x) :=
-begin
-  apply le_antisymm,
-  { apply nhds_within_mono,
-    simp only with mfld_simps},
-  { apply nhds_within_le_of_mem (ext_chart_at_target_mem_nhds_within _ _) }
-end
+(nhds_within_mono _ (ext_chart_at_target_subset_range _ _)).antisymm $
+  nhds_within_le_of_mem (ext_chart_at_target_mem_nhds_within _ _)
 
-lemma ext_chart_continuous_at_symm' {x' : M} (h : x' ∈ (ext_chart_at I x).source) :
-  continuous_at (ext_chart_at I x).symm ((ext_chart_at I x) x') :=
+lemma ext_chart_continuous_at_symm'' {y : E} (h : y ∈ (ext_chart_at I x).target) :
+  continuous_at (ext_chart_at I x).symm y :=
 begin
   apply continuous_at.comp,
-  { rw ext_chart_at_source at h,
-    simp only with mfld_simps,
-    exact ((chart_at H x).continuous_on_symm _
-      ((chart_at H x).map_source h)).continuous_at
-        (mem_nhds_sets (chart_at H x).open_target
-          ((chart_at H x).map_source h)) },
+  { suffices : continuous_at (chart_at H x).symm (I.symm y), by simpa only with mfld_simps,
+    refine (chart_at H x).continuous_at_symm _,
+    simp only with mfld_simps at h,
+    exact h.2 },
   { exact I.continuous_symm.continuous_at }
 end
 
+lemma ext_chart_continuous_at_symm' {x' : M} (h : x' ∈ (ext_chart_at I x).source) :
+  continuous_at (ext_chart_at I x).symm (ext_chart_at I x x') :=
+ext_chart_continuous_at_symm'' I _ $ (ext_chart_at I x).map_source h
+
 lemma ext_chart_continuous_at_symm :
   continuous_at (ext_chart_at I x).symm ((ext_chart_at I x) x) :=
 ext_chart_continuous_at_symm' I x (mem_ext_chart_source I x)
 
+lemma ext_chart_continuous_on_symm :
+  continuous_on (ext_chart_at I x).symm (ext_chart_at I x).target :=
+λ y hy, (ext_chart_continuous_at_symm'' _ _ hy).continuous_within_at
+
 /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
 in the source is a neighborhood of the preimage, within a set. -/
 lemma ext_chart_preimage_mem_nhds_within' {x' : M} (h : x' ∈ (ext_chart_at I x).source)
diff --git a/src/geometry/manifold/times_cont_mdiff.lean b/src/geometry/manifold/times_cont_mdiff.lean
index 1bb79eec5f78c..8d15848c0c18e 100644
--- a/src/geometry/manifold/times_cont_mdiff.lean
+++ b/src/geometry/manifold/times_cont_mdiff.lean
@@ -284,8 +284,48 @@ lemma smooth_within_at_iff_target :
     (s ∩ f ⁻¹' (ext_chart_at I' (f x)).source) x :=
 times_cont_mdiff_within_at_iff_target
 
+lemma times_cont_mdiff_at_ext_chart_at :
+  times_cont_mdiff_at I 𝓘(𝕜, E) n (ext_chart_at I x) x :=
+begin
+  rw [times_cont_mdiff_at, times_cont_mdiff_within_at_iff],
+  refine ⟨(ext_chart_at_continuous_at _ _).continuous_within_at, _⟩,
+  refine times_cont_diff_within_at_id.congr _ _;
+    simp only with mfld_simps { contextual := tt }
+end
+
 include Is I's
 
+/-- One can reformulate smoothness within a set at a point as continuity within this set at this
+point, and smoothness in the corresponding extended chart. -/
+lemma times_cont_mdiff_within_at_iff' {x' : M} {y : M'} (hx : x' ∈ (chart_at H x).source)
+  (hy : f x' ∈ (chart_at H' y).source) :
+  times_cont_mdiff_within_at I I' n f s x' ↔ continuous_within_at f s x' ∧
+    times_cont_diff_within_at 𝕜 n ((ext_chart_at I' y) ∘ f ∘ (ext_chart_at I x).symm)
+    ((ext_chart_at I x).target ∩ (ext_chart_at I x).symm ⁻¹' (s ∩ f ⁻¹' (ext_chart_at I' y).source))
+    (ext_chart_at I x x') :=
+begin
+  refine ((times_cont_diff_within_at_local_invariant_prop I I' n).lift_prop_within_at_indep_chart
+    (structure_groupoid.chart_mem_maximal_atlas _ x) hx
+    (structure_groupoid.chart_mem_maximal_atlas _ y) hy).trans _,
+  rw [times_cont_diff_within_at_prop, iff_eq_eq],
+  congr' 2,
+  mfld_set_tac
+end
+
+omit I's
+
+lemma times_cont_mdiff_at_ext_chart_at' {x' : M} (h : x' ∈ (chart_at H x).source) :
+  times_cont_mdiff_at I 𝓘(𝕜, E) n (ext_chart_at I x) x' :=
+begin
+  refine (times_cont_mdiff_within_at_iff' h (mem_chart_source _ _)).2 _,
+  refine ⟨(ext_chart_at_continuous_at' _ _ _).continuous_within_at, _⟩,
+  { rwa ext_chart_at_source },
+  refine times_cont_diff_within_at_id.congr' _ _;
+    simp only [h] with mfld_simps { contextual := tt }
+end
+
+include I's
+
 /-- One can reformulate smoothness on a set as continuity on this set, and smoothness in any
 extended chart. -/
 lemma times_cont_mdiff_on_iff :