feat: Sum.inl and Sum.inr are smooth embeddings (leanprover-community#40507)

This provides an alternative proof of their smoothness. A future PR will use this to golf the existing proofs.

Inspired by in-person discussions with Christian Merten and Edward van de Meent.

Author: grunweg

Mathlib/Geometry/Manifold/Immersion.lean

@@ -54,6 +54,8 @@ This shortens the overall argument, as the definition of submersions has the sam
 * `IsImmersion.id`: the identity map is an immersion
 * `IsImmersion.of_opens`: the inclusion of an open subset `s → M` of a smooth manifold
   is a smooth immersion
+* `IsImmersionOfComplement.sumInl` and `IsImmersionOfComplement.sumInr`: given `C^n` manifolds
+  `M` and `N`, `Sum.inl : M → M ⊕ N` and `Sum.inr : N → M ⊕ N` are `C^n` immersions
 * `IsImmersionAt.contMDiffAt`: if f is an immersion at `x`, it is `C^n` at `x`.
 * `IsImmersion.contMDiff`: if f is a `C^n` immersion, it is automatically `C^n`
   in the sense of `ContMDiff`.
@@ -615,6 +617,7 @@ In other words, `f` is an immersion at each `x ∈ M`.
 This definition has a fixed parameter `F`, which is a choice of complement of `E` in `E'`:
 being an immersion at `x` includes a choice of linear isomorphism between `E × F` and `E'`.
 -/
+@[expose]
 def IsImmersionOfComplement (f : M → N) : Prop := ∀ x, IsImmersionAtOfComplement F I J n f x
 
 variable (I J n) in
@@ -696,6 +699,32 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) :
     IsImmersionOfComplement PUnit I I n (Subtype.val : s → M) :=
   fun y ↦ IsImmersionAtOfComplement.of_opens s y
 
+/-- Given `C^n` manifolds `M` and `N` over the same model `I`,
+`Sum.inl : M → M ⊕ N` is a `C^n` immersion with complement `Unit` -/
+lemma sumInl {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I n M]
+    [IsManifold I n M'] : IsImmersionOfComplement Unit I I n (@Sum.inl M M') := by
+  intro x
+  apply IsImmersionAtOfComplement.mk_of_continuousAt (equiv := (.prodUnique 𝕜 E _))
+    (by fun_prop) _ _ (mem_chart_source H x) (mem_chart_source H (Sum.inl x))
+    (IsManifold.chart_mem_maximalAtlas x) (IsManifold.chart_mem_maximalAtlas (Sum.inl x))
+  intro y hy
+  have : I ((chartAt H x) ((chartAt H x).symm (I.symm y))) = y := by
+    rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
+  simpa
+
+/-- Given `C^n` manifolds `M` and `N` over the same model `I`,
+`Sum.inr : N → M ⊕ N` is a `C^n` immersion with complement `Unit` -/
+lemma sumInr {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M'] [IsManifold I n M]
+    [IsManifold I n M'] : IsImmersionOfComplement Unit I I n (@Sum.inr M M') := by
+  intro x
+  apply IsImmersionAtOfComplement.mk_of_continuousAt (equiv := (.prodUnique 𝕜 E _))
+    (by fun_prop) _ _ (mem_chart_source H x) (mem_chart_source H (Sum.inr x))
+    (IsManifold.chart_mem_maximalAtlas x) (IsManifold.chart_mem_maximalAtlas (Sum.inr x))
+  intro y hy
+  have : I ((chartAt H x) ((chartAt H x).symm (I.symm y))) = y := by
+    rw [(chartAt H x).right_inv (by simp_all), I.right_inv (by simp_all)]
+  simpa
+
 @[deprecated (since := "2025-12-16")] alias ofOpen := of_opens
 
 /-- A `C^n` immersion is `C^n`. -/

Mathlib/Geometry/Manifold/SmoothEmbedding.lean

@@ -22,6 +22,8 @@ This will be useful to define embedded submanifolds.
 * `IsSmoothEmbedding.id`: the identity map is a smooth embedding
 * `IsSmoothEmbedding.of_opens`: the inclusion of an open subset `s → M` of a smooth manifold
   is a smooth embedding
+* `IsSmoothEmbedding.sumInl` and `IsSmoothEmbedding.sumInr`: given `C^n` manifolds `M` and `N`,
+  `Sum.inl : M → M ⊕ N` and `Sum.inr : N → M ⊕ N` are `C^n` embeddings
 * `IsSmoothEmbedding.contMDiff`: if `f` is a `C^n` embedding, it is automatically `C^n`
   in the sense of `ContMDiff`.
 
@@ -92,6 +94,16 @@ lemma of_opens [IsManifold I n M] (s : TopologicalSpace.Opens M) :
   rw [isSmoothEmbedding_iff]
   exact ⟨IsImmersion.of_opens s, IsEmbedding.subtypeVal⟩
 
+/-- Given `C^n` manifolds `M` and `N`, `Sum.inl : M → M ⊕ N` is a `C^n` embedding. -/
+lemma sumInl {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M']
+    [IsManifold I n M] [IsManifold I n M'] : IsSmoothEmbedding I I n (@Sum.inl M M') :=
+  ⟨IsImmersionOfComplement.sumInl.isImmersion, Topology.IsEmbedding.inl⟩
+
+/-- Given `C^n` manifolds `M` and `N`, `Sum.inr : N → M ⊕ N` is a `C^n` embedding. -/
+lemma sumInr {M' : Type*} [TopologicalSpace M'] [ChartedSpace H M']
+    [IsManifold I n M] [IsManifold I n M'] : IsSmoothEmbedding I I n (@Sum.inr M M') :=
+  ⟨IsImmersionOfComplement.sumInr.isImmersion, Topology.IsEmbedding.inr⟩
+
 /-- A smooth embedding is automatically smooth. -/
 lemma contMDiff (hf : IsSmoothEmbedding I J n f) :
     ContMDiff I J n f :=