feat: add custom elaborators for immersions

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -909,6 +909,12 @@ theorem contDiffWithinAt_fst {s : Set (E × F)} {p : E × F} :
     ContDiffWithinAt 𝕜 n (Prod.fst : E × F → E) s p :=
   contDiff_fst.contDiffWithinAt
 
+/-- Postcomposing `f` with `Prod.fst` is `C^n` at `x` -/
+@[fun_prop]
+theorem ContDiffWithinAt.fst {f : E → F × G} {x : E} (hf : ContDiffWithinAt 𝕜 n f s x) :
+    ContDiffWithinAt 𝕜 n (fun x => (f x).1) (s) x :=
+  contDiffWithinAt_fst.comp x hf (mapsTo_image f s)
+
 /-- The second projection in a product is `C^∞`. -/
 @[fun_prop]
 theorem contDiff_snd : ContDiff 𝕜 n (Prod.snd : E × F → F) :=
@@ -933,11 +939,23 @@ theorem ContDiffOn.snd {f : E → F × G} {s : Set E} (hf : ContDiffOn 𝕜 n f
     ContDiffOn 𝕜 n (fun x => (f x).2) s :=
   contDiff_snd.comp_contDiffOn hf
 
+/-- The second projection at a point in a product is `C^∞`. -/
+@[fun_prop]
+theorem contDiffWithinAt_snd {s : Set (E × F)} {p : E × F} :
+    ContDiffWithinAt 𝕜 n (Prod.snd : E × F → F) s p :=
+  contDiff_snd.contDiffWithinAt
+
 /-- The second projection at a point in a product is `C^∞`. -/
 @[fun_prop]
 theorem contDiffAt_snd {p : E × F} : ContDiffAt 𝕜 n (Prod.snd : E × F → F) p :=
   contDiff_snd.contDiffAt
 
+/-- Postcomposing `f` with `Prod.snd` is `C^n` at `x` -/
+@[fun_prop]
+theorem ContDiffWithinAt.snd {f : E → F × G} {x : E} (hf : ContDiffWithinAt 𝕜 n f s x) :
+    ContDiffWithinAt 𝕜 n (fun x => (f x).2) (s) x :=
+  contDiffWithinAt_snd.comp x hf (mapsTo_image f s)
+
 /-- Postcomposing `f` with `Prod.snd` is `C^n` at `x` -/
 @[fun_prop]
 theorem ContDiffAt.snd {f : E → F × G} {x : E} (hf : ContDiffAt 𝕜 n f x) :
@@ -954,11 +972,25 @@ theorem ContDiffAt.snd'' {f : F → G} {x : E × F} (hf : ContDiffAt 𝕜 n f x.
     ContDiffAt 𝕜 n (fun x : E × F => f x.2) x :=
   hf.comp x contDiffAt_snd
 
-/-- The second projection within a domain at a point in a product is `C^∞`. -/
-@[fun_prop]
-theorem contDiffWithinAt_snd {s : Set (E × F)} {p : E × F} :
-    ContDiffWithinAt 𝕜 n (Prod.snd : E × F → F) s p :=
-  contDiff_snd.contDiffWithinAt
+theorem contDiffWithinAt_prod_iff (f : E → F × G) :
+    ContDiffWithinAt 𝕜 n f s x ↔
+      ContDiffWithinAt 𝕜 n (Prod.fst ∘ f) s x ∧ ContDiffWithinAt 𝕜 n (Prod.snd ∘ f) s x :=
+  ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩
+
+theorem contDiffAt_prod_iff (f : E → F × G) :
+    ContDiffAt 𝕜 n f x ↔
+      ContDiffAt 𝕜 n (Prod.fst ∘ f) x ∧ ContDiffAt 𝕜 n (Prod.snd ∘ f) x :=
+  ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩
+
+theorem contDiffOn_prod_iff (f : E → F × G) :
+    ContDiffOn 𝕜 n f s ↔
+      ContDiffOn 𝕜 n (Prod.fst ∘ f) s ∧ ContDiffOn 𝕜 n (Prod.snd ∘ f) s :=
+  ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩
+
+theorem contDiff_prod_iff (f : E → F × G) :
+    ContDiff 𝕜 n f ↔
+      ContDiff 𝕜 n (Prod.fst ∘ f) ∧ ContDiff 𝕜 n (Prod.snd ∘ f) :=
+  ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.1.prodMk h.2⟩
 
 section NAry
 

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

@@ -6,12 +6,23 @@ Authors: Sébastien Gouëzel, Floris van Doorn
 module
 
 public import Mathlib.Geometry.Manifold.ContMDiff.Basic
+import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
 
 /-!
-## Smoothness of charts and local structomorphisms
+# Smoothness of charts and local structomorphisms
 
 We show that the model with corners, charts, extended charts and their inverses are `C^n`,
 and that local structomorphisms are `C^n` with `C^n` inverses.
+
+## Implementation notes
+
+This file uses the name `writtenInExtend` (in analogy to `writtenInExtChart`) to refer to a
+composition `ψ.extend J ∘ f ∘ φ.extend I` of `f : M → N` with charts `ψ` and `φ` extended by the
+appropriate models with corners. This is not a definition, so technically deviating from the naming
+convention.
+
+`isLocalStructomorphOn` is another made-up name.
+
 -/
 
 @[expose] public section
@@ -89,8 +100,12 @@ theorem contMDiffAt_extChartAt : ContMDiffAt I 𝓘(𝕜, E) n (extChartAt I x)
   filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
   exact PartialEquiv.right_inv (extChartAt I x) hy
 
+theorem contMDiffOn_extend (he : e ∈ maximalAtlas I n M) :
+    ContMDiffOn I 𝓘(𝕜, E) n (e.extend I) e.source :=
+  fun _x' hx' ↦ (contMDiffAt_extend he hx').contMDiffWithinAt
+
 theorem contMDiffOn_extChartAt : ContMDiffOn I 𝓘(𝕜, E) n (extChartAt I x) (chartAt H x).source :=
-  fun _x' hx' => (contMDiffAt_extChartAt' hx').contMDiffWithinAt
+  contMDiffOn_extend (chart_mem_maximalAtlas x)
 
 theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I n M) :
     ContMDiffOn 𝓘(𝕜, E) I n (e.extend I).symm (I '' e.target) := by
@@ -289,3 +304,34 @@ theorem isLocalStructomorphOn_contDiffGroupoid_iff (f : OpenPartialHomeomorph M
     · simp only [c, c', hx', mfld_simps]
 
 end IsLocalStructomorph
+
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type*} [TopologicalSpace G]
+  {J : ModelWithCorners 𝕜 F G} {N : Type*} [TopologicalSpace N] [ChartedSpace G N]
+  {n : WithTop ℕ∞}
+  [IsManifold I n M] [IsManifold J n N] {f : M → N} {s : Set M}
+  {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G}
+
+/-- This is a smooth analogue of `OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff`. -/
+theorem contMDiffWithinAt_writtenInExtend_iff {y : M}
+    (hφ : φ ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N)
+    (hy : y ∈ φ.source) (hgy : f y ∈ ψ.source) (hmaps : MapsTo f s ψ.source) :
+    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (ψ.extend J ∘ f ∘ (φ.extend I).symm)
+      ((φ.extend I).symm ⁻¹' s ∩ range I) (φ.extend I y) ↔ ContMDiffWithinAt I J n f s y := by
+  rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hφ hψ hy hgy]
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩
+  · rw [← φ.continuousWithinAt_writtenInExtend_iff (I := I) (I' := J) hy hgy hmaps]
+    exact h.continuousWithinAt
+  · rwa [← contMDiffWithinAt_iff_contDiffWithinAt]
+  · rw [contMDiffWithinAt_iff_contDiffWithinAt]
+    exact h.2
+
+theorem contMDiffOn_writtenInExtend_iff (hφ : φ ∈ maximalAtlas I n M) (hψ : ψ ∈ maximalAtlas J n N)
+    (hs : s ⊆ φ.source) (hmaps : MapsTo f s ψ.source) :
+    ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, F) n (ψ.extend J ∘ f ∘ (φ.extend I).symm) (φ.extend I '' s) ↔
+      ContMDiffOn I J n f s := by
+  refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_
+  refine (contMDiffWithinAt_congr_set ?_).trans
+    (contMDiffWithinAt_writtenInExtend_iff hφ hψ (hs hx) (hmaps hx) hmaps)
+  rw [← nhdsWithin_eq_iff_eventuallyEq, ← φ.map_extend_nhdsWithin_eq_image_of_subset,
+    ← φ.map_extend_nhdsWithin]
+  exacts [hs hx, hs hx, hs]