From c93d43b901186c00b95c28fdb1bf8b3437b64577 Mon Sep 17 00:00:00 2001
From: Marygold-Dusk <naranjosamantha1j@gmail.com>
Date: Wed, 11 Feb 2026 10:07:24 +0100
Subject: [PATCH 01/18] Submersions

---
 Mathlib/Geometry/Manifold/Submersion.lean | 573 ++++++++++++++++++++++
 1 file changed, 573 insertions(+)
 create mode 100644 Mathlib/Geometry/Manifold/Submersion.lean

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
new file mode 100644
index 00000000000000..db98465c589249
--- /dev/null
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -0,0 +1,573 @@
+/-
+Copyright (c) 2025 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Rothgang
+-/
+import Mathlib.Geometry.Manifold.Immersion
+
+/-! # Smooth submersions
+
+In this file, we define `C^n` submersions between `C^n` manifolds.
+As in the case of immersions, the correct definition in the infinite-dimensional setting differs
+from the classical finite-dimensional one (which is usually phrased in terms of surjectivity of the
+`mfderiv`).
+
+Our definition was formulated in terms of local normal forms; i.e.,
+a map `f` is a submersion at `x` if there exist charts near `x` and `f x` in which `f`
+has the standard projection `(u, v) ↦ u`, after identifying the model space of the domain with
+a product `E ≃L[𝕜] (E'' × F)`.
+
+The results in this file follow from abstract results about such local properties.
+
+## Main definitions
+
+* `IsSubmersionAtOfComplement F I J n f x` means a map `f : M → N` between `C^n` manifolds `M` and
+  `N` is a submersion at `x : M`: there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`,
+  respectively, such that in these charts, `f` looks like `(u, v) ↦ u`, w.r.t. some equivalence
+  `E ≃L[𝕜] (E'' × F)`. Differentiability of `f` is not assumed as it follows from this definition.
+* `IsSubmersionAt I J n f x` means that `f` is a `C^n` submersion at `x : M` for some choice of a
+  complement `F` of the model normed space `E` of `M` in the model normed space `E'` of `N`.
+* `IsSubmersionOfComplement F I J n f` means `f : M → N` is a submersion at every point `x : M`,
+  w.r.t. the chosen complement `F`.
+* `IsSubmersion I J n f` means `f : M → N` is a submersion at every point `x : M`,
+  w.r.t. some global choice of complement.
+
+## Main results
+
+* `IsSubmersionAt.congr_of_eventuallyEq`: being a submersion is a local property.
+  If `f` and `g` agree near `x` and `f` is a submersion at `x`, then so is `g`.
+* `IsSubmersionAtOfComplement.congr_F`, `IsSubmersionOfComplement.congr_F`:
+  being a submersion at `x` w.r.t. `F` is stable under
+  replacing the complement `F` by a continuously linearly equivalent copy of `F`.
+* `isOpen_isSubmersionAtOfComplement` and `isOpen_isSubmersionAt`:
+  the set of points where `IsSubmersionAt(OfComplement)` holds is open.
+* `IsSubmersionAt.prodMap` and `IsSubmersion.prodMap`: the product of two submersions at a point
+  is an submersion at the product point.
+
+## Implementation notes
+
+* Universe management tools (`small`, `smallComplement`, `smallEquiv`) ensure that
+  complements can always be chosen in the correct universe, which is essential for
+  existential definitions such as `isSubmersionAt`.
+* In most applications, there is no need to control the choice of complement in the definition of a
+  submersion, so `IsSubmersion(At)` is perfectly adequate. Nevertheless, explicit control over
+  complements becomes useful when studying the local characterisation of submanifolds. Locally,
+  a submanifold can be described either as the image of a submersion or as the preimage of
+  an immersion, and this equivalence requires working with the same choice of complement.
+  Providing a version of the definition that includes complements allows this equivalence to be
+  stated cleanly.
+* To avoid a free universe variable in `IsSubmersion(At)`, we require the complement to be taken in
+  the same universe as the model normed space for `N`. We also offer convenience constructors that
+  relax this requirement to preserve usability. This relies on the observation that the equivalence
+  in the definition of immersions allows the universe of the complement to be reduced,
+  as implemented in `IsImmersion(At)OfComplement.small`
+  and  `IsImmersion(At)OfComplement.smallEquiv`.
+
+## TODO
+* `IsSubmersionAt.contMDiffAt`: if f is a submersion at `x`, it is a `C^n` map at `x`.
+* `IsSubmersion.contMDiff`: if f is a submersion, it is `C^n` map.
+
+**Please do not work** on this file without prior discussion with Michael Rothgang.
+This will be the topic of Samantha Naranjo's master's thesis, and it's nice to coordinate.
+-/
+
+noncomputable section
+
+open scoped Topology ContDiff
+
+open Function Set Manifold
+
+universe u
+
+variable {𝕜 E' E'' E''' F F' H H' G G' : Type*} {E : Type u} [NontriviallyNormedField 𝕜]
+  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
+  [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [NormedAddCommGroup E'''] [NormedSpace 𝕜 E''']
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup F'] [NormedSpace 𝕜 F']
+  [TopologicalSpace H] [TopologicalSpace H'] [TopologicalSpace G] [TopologicalSpace G']
+  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
+  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'}
+
+variable {M M' N N' : Type*}
+  [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [ChartedSpace H' M']
+  [TopologicalSpace N] [ChartedSpace G N] [TopologicalSpace N'] [ChartedSpace G' N']
+  {n : WithTop ℕ∞}
+
+variable (F I J M N) in
+/-- The local property of being a submersion at `x` -/
+def SubmersionAtProp :
+    ((M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop) :=
+  fun f domChart codChart ↦
+    ∃ equiv : E ≃L[𝕜] (E'' × F),
+    EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
+      (domChart.extend I).target
+
+omit [ChartedSpace H M] [ChartedSpace G N] in
+/-- Being a submersion at `x` is a local property. -/
+lemma isLocalSourceTargetProperty_submmersionAtProp :
+    IsLocalSourceTargetProperty (SubmersionAtProp F I J M N) where
+  mono_source {f φ ψ s} hs := fun ⟨equiv, hf⟩ ↦ ⟨equiv, hf.mono (by simp; grind)⟩
+  congr {f g φ ψ} hfg hf := by
+    obtain ⟨equiv, hf⟩ := hf
+    refine ⟨equiv, EqOn.trans (fun x hx ↦ ?_) (hf.mono (by simp))⟩
+    have : ((φ.extend I).symm) x ∈ φ.source := by simp_all
+    grind
+
+variable (F I J n) in
+/-- `f : M → N` is a `C^k` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
+around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
+Additionally, we demand that `f` map `φ.source` into `ψ.source`.
+
+NB. We don't know the particular atlasses used for `M` and `N`, so asking for `φ` and `ψ` to be
+in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficient.
+-/
+irreducible_def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=
+  LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N)
+
+irreducible_def IsSubmersionAt (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G)
+    (n : WithTop ℕ∞) (f : M → N) (x : M) : Prop :=
+  ∃ (F : Type u) (_ : NormedAddCommGroup F) (_ : NormedSpace 𝕜 F),
+    IsSubmersionAtOfComplement F I J n f x
+
+variable {f g : M → N} {x : M}
+namespace IsSubmersionAtOfComplement
+
+lemma mk_of_charts (equiv : E ≃L[𝕜] (E'' × F)) (domChart : OpenPartialHomeomorph M H)
+    (codChart : OpenPartialHomeomorph N G)
+    (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source)
+    (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M)
+    (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N)
+    (hsource : domChart.source ⊆ f ⁻¹' codChart.source)
+    (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
+      (domChart.extend I).target) : IsSubmersionAtOfComplement F I J n f x := by
+  rw [IsSubmersionAtOfComplement_def]
+  use domChart, codChart
+  use equiv
+
+lemma mk_of_continuousAt {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv : E ≃L[𝕜] (E'' × F))
+    (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G)
+    (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source)
+    (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M)
+    (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N)
+    (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
+      (domChart.extend I).target) : IsSubmersionAtOfComplement F I J n f x := by
+  rw [IsSubmersionAtOfComplement_def]
+  exact LiftSourceTargetPropertyAt.mk_of_continuousAt hf
+    isLocalSourceTargetProperty_submmersionAtProp
+    _ _ hx hfx hdomChart hcodChart ⟨equiv, hwrittenInExtend⟩
+
+def domChart (h : IsSubmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph M H := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact LiftSourceTargetPropertyAt.domChart h
+
+def codChart (h : IsSubmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph N G := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact LiftSourceTargetPropertyAt.codChart h
+
+lemma mem_domChart_source (h : IsSubmersionAtOfComplement F I J n f x) : x ∈ h.domChart.source := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact LiftSourceTargetPropertyAt.mem_domChart_source h
+
+lemma mem_codChart_source (h : IsSubmersionAtOfComplement F I J n f x) :
+    f x ∈ h.codChart.source := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact LiftSourceTargetPropertyAt.mem_codChart_source h
+
+lemma domChart_mem_maximalAtlas (h : IsSubmersionAtOfComplement F I J n f x) :
+    h.domChart ∈ IsManifold.maximalAtlas I n M := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas h
+
+lemma codChart_mem_maximalAtlas (h : IsSubmersionAtOfComplement F I J n f x) :
+    h.codChart ∈ IsManifold.maximalAtlas J n N := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas h
+
+lemma source_subset_preimage_source (h : IsSubmersionAtOfComplement F I J n f x) :
+    h.domChart.source ⊆ f ⁻¹' h.codChart.source := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact LiftSourceTargetPropertyAt.source_subset_preimage_source h
+
+def equiv (h : IsSubmersionAtOfComplement F I J n f x) : E ≃L[𝕜] (E'' × F) := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact Classical.choose <| LiftSourceTargetPropertyAt.property h
+
+lemma writtenInCharts (h : IsSubmersionAtOfComplement F I J n f x) :
+    EqOn ((h.codChart.extend J) ∘ f ∘ (h.domChart.extend I).symm) (Prod.fst ∘ h.equiv)
+      (h.domChart.extend I).target := by
+  rw [IsSubmersionAtOfComplement_def] at h
+  exact Classical.choose_spec <| LiftSourceTargetPropertyAt.property h
+
+lemma property (h : IsSubmersionAtOfComplement F I J n f x) :
+    LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N) := by
+  rwa [IsSubmersionAtOfComplement_def] at h
+
+lemma map_target_subset_target (h : IsSubmersionAtOfComplement F I J n f x) :
+    (Prod.fst ∘ h.equiv) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target := by
+  rw [← h.writtenInCharts.image_eq, Set.image_comp, Set.image_comp,
+    PartialEquiv.symm_image_target_eq_source, OpenPartialHomeomorph.extend_source,
+    ← PartialEquiv.image_source_eq_target]
+  have : f '' h.domChart.source ⊆ h.codChart.source := by
+    simp [h.source_subset_preimage_source]
+  grw [this, OpenPartialHomeomorph.extend_source]
+
+lemma target_subset_preimage_target (h : IsSubmersionAtOfComplement F I J n f x) :
+    (h.domChart.extend I).target ⊆ (Prod.fst ∘ h.equiv) ⁻¹' (h.codChart.extend J).target :=
+  fun _x hx ↦ h.map_target_subset_target (mem_image_of_mem _ hx)
+
+lemma congr_of_eventuallyEq (hf : IsSubmersionAtOfComplement F I J n f x) (hfg : f =ᶠ[𝓝 x] g) :
+    IsSubmersionAtOfComplement F I J n g x := by
+  rw [IsSubmersionAtOfComplement_def]
+  exact LiftSourceTargetPropertyAt.congr_of_eventuallyEq
+    isLocalSourceTargetProperty_submmersionAtProp hf.property hfg
+
+lemma congr_iff_of_eventuallyEq (hfg : f =ᶠ[𝓝 x] g) :
+    IsSubmersionAtOfComplement F I J n f x ↔ IsSubmersionAtOfComplement F I J n g x := by
+  simpa only [IsSubmersionAtOfComplement_def] using
+    LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq
+      isLocalSourceTargetProperty_submmersionAtProp hfg
+
+lemma small (hf : IsSubmersionAtOfComplement F I J n f x) : Small.{u} F :=
+  small_of_injective <| hf.equiv.symm.injective.comp (Prod.mk_right_injective 0)
+
+/-- Given a submersion `f` at `x`, this is a choice of complement which lives in the same universe
+as the model space for the domain of `f`: this is useful to avoid universe restrictions. -/
+def smallComplement (hf : IsSubmersionAtOfComplement F I J n f x) : Type u :=
+  haveI := hf.small
+  Shrink.{u} F
+
+instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement := by
+  haveI := hf.small
+  unfold smallComplement
+  infer_instance
+
+instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement := by
+  haveI := hf.small
+  unfold smallComplement
+  infer_instance
+
+/-- Given an submersion `f` at `x` w.r.t. a complement `F`, this construction provides
+a continuous linear equivalence from `F` to the small complement of `F`:
+mathematically, this is just the identity map; however, this is technically useful as it enables
+us to always work with `hf.smallComplement`. -/
+def smallEquiv (hf : IsSubmersionAtOfComplement F I J n f x) : F ≃L[𝕜] hf.smallComplement :=
+  haveI := hf.small
+  ((equivShrink F).symm.continuousLinearEquiv 𝕜).symm
+
+lemma trans_F (h : IsSubmersionAtOfComplement F I J n f x) (e : F ≃L[𝕜] F') :
+    IsSubmersionAtOfComplement F' I J n f x := by
+  rw [IsSubmersionAtOfComplement_def]
+  refine ⟨h.domChart, h.codChart, h.mem_domChart_source, h.mem_codChart_source,
+    h.domChart_mem_maximalAtlas, h.codChart_mem_maximalAtlas, h.source_subset_preimage_source, ?_⟩
+  use h.equiv.trans ((ContinuousLinearEquiv.refl 𝕜 E'').prodCongr e)
+  apply Set.EqOn.trans h.writtenInCharts
+  intro x hx
+  simp
+
+/-- Being an submersion at `x` w.r.t. `F` is stable under replacing `F` by an isomorphic copy. -/
+lemma congr_F (e : F ≃L[𝕜] F') :
+    IsSubmersionAtOfComplement F I J n f x ↔ IsSubmersionAtOfComplement F' I J n f x :=
+  ⟨fun h ↦ trans_F (e := e) h, fun h ↦ trans_F (e := e.symm) h⟩
+
+/- The set of points where `IsSubmersionAtOfComplement` holds is open. -/
+lemma _root_.isOpen_isSubmersionAt :
+    IsOpen {x | IsSubmersionAtOfComplement F I J n f x} := by
+  simp_rw [IsSubmersionAtOfComplement_def]
+  exact IsOpen.liftSourceTargetPropertyAt
+
+/-- If `f: M → N` and `g: M' × N'` are submersions at `x` and `x'`, respectively,
+then `f × g: M × N → M' × N'` is an submersion at `(x, x')`. -/
+theorem prodMap {f : M → N} {g : M' → N'} {x' : M'}
+    [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N']
+    (hf : IsSubmersionAtOfComplement F I J n f x)
+    (hg : IsSubmersionAtOfComplement F' I' J' n g x') :
+    IsSubmersionAtOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x') := by
+  let P := SubmersionAtProp F I J M N
+  let Q := SubmersionAtProp F' I' J' M' N'
+  let R := SubmersionAtProp (F × F') (I.prod I') (J.prod J') (M × M') (N × N')
+  -- This is the key proof: submersions are stable under products.
+  have key : ∀ {f : M → N}, ∀ {φ₁ : OpenPartialHomeomorph M H}, ∀ {ψ₁ : OpenPartialHomeomorph N G},
+      ∀ {g : M' → N'}, ∀ {φ₂ : OpenPartialHomeomorph M' H'}, ∀ {ψ₂ : OpenPartialHomeomorph N' G'},
+      P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂) := by
+    rintro f φ₁ ψ₁ g φ₂ ψ₂ ⟨equiv₁, hfprop⟩ ⟨equiv₂, hgprop⟩
+    use (equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')
+    rw [φ₁.extend_prod φ₂, ψ₁.extend_prod, PartialEquiv.prod_target]
+    set C := ((ψ₁.extend J).prod (ψ₂.extend J')) ∘
+      Prod.map f g ∘ ((φ₁.extend I).prod (φ₂.extend I')).symm
+    have hC : C = Prod.map ((ψ₁.extend J) ∘ f ∘ (φ₁.extend I).symm)
+        ((ψ₂.extend J') ∘ g ∘ (φ₂.extend I').symm) := by
+      ext x <;> simp [C]
+    set Φ := Prod.fst ∘ ((equiv₁.prodCongr equiv₂).trans
+      (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F'))
+    have hΦ: Φ = Prod.map (Prod.fst ∘ equiv₁) (Prod.fst ∘ equiv₂) := by ext x <;> simp [Φ]
+    rw [hC, hΦ]
+    exact hfprop.prodMap hgprop
+  rw [IsSubmersionAtOfComplement_def]
+  exact LiftSourceTargetPropertyAt.prodMap hf.property hg.property key
+
+/-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`.
+-/
+lemma isSubmersionAt (h : IsSubmersionAtOfComplement F I J n f x) :
+    IsSubmersionAt I J n f x := by
+  rw [IsSubmersionAt_def]
+  use h.smallComplement, by infer_instance, by infer_instance
+  exact (IsSubmersionAtOfComplement.congr_F h.smallEquiv).mp h
+
+end IsSubmersionAtOfComplement
+
+namespace IsSubmersionAt
+
+lemma mk_of_charts (equiv : E ≃L[𝕜] (E'' × F))
+    (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G)
+    (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source)
+    (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M)
+    (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N)
+    (hsource : domChart.source ⊆ f ⁻¹' codChart.source)
+    (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
+      (domChart.extend I).target) : IsSubmersionAt I J n f x := by
+  rw [IsSubmersionAt_def]
+  have aux : IsSubmersionAtOfComplement F I J n f x := by
+    apply IsSubmersionAtOfComplement.mk_of_charts <;> assumption
+  use aux.smallComplement, by infer_instance, by infer_instance
+  rwa [← IsSubmersionAtOfComplement.congr_F aux.smallEquiv]
+
+/-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
+around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
+This version does not assume that `f` maps `φ.source` to `ψ.source`,
+but that `f` is continuous at `x`. -/
+lemma mk_of_continuousAt {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv : E ≃L[𝕜] (E'' × F))
+    (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G)
+    (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source)
+    (hdomChart : domChart ∈ IsManifold.maximalAtlas I n M)
+    (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N)
+    (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
+      (domChart.extend I).target) : IsSubmersionAt I J n f x := by
+  rw [IsSubmersionAt_def]
+  have aux : IsSubmersionAtOfComplement F I J n f x := by
+    apply IsSubmersionAtOfComplement.mk_of_continuousAt <;> assumption
+  use aux.smallComplement, by infer_instance, by infer_instance
+  rwa [← IsSubmersionAtOfComplement.congr_F aux.smallEquiv]
+
+/-- A choice of complement of the model normed space `E` of `M` in the model normed space
+`E'` of `N` -/
+def complement (h : IsSubmersionAt I J n f x) : Type u := by
+  rw [IsSubmersionAt_def] at h
+  exact Classical.choose h
+
+noncomputable instance (h : IsSubmersionAt I J n f x) : NormedAddCommGroup h.complement := by
+  rw [IsSubmersionAt_def] at h
+  exact Classical.choose <| Classical.choose_spec h
+
+noncomputable instance (h : IsSubmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by
+  rw [IsSubmersionAt_def] at h
+  exact Classical.choose <| Classical.choose_spec <| Classical.choose_spec h
+
+lemma isSubmersionAtOfComplement_complement (h : IsSubmersionAt I J n f x) :
+    IsSubmersionAtOfComplement h.complement I J n f x := by
+  rw [IsSubmersionAt_def] at h
+  exact Classical.choose_spec <| Classical.choose_spec <| Classical.choose_spec h
+
+/-- A choice of chart on the domain `M` of a submersion `f` at `x`:
+w.r.t. this chart and the data `h.codChart` and `h.equiv`,
+`f` will look like a projection `(u, v) ↦ u` in these extended charts.
+The particular chart is arbitrary, but this choice matches the witnesses given by
+`h.codChart` and `h.codChart`. -/
+def domChart (h : IsSubmersionAt I J n f x) : OpenPartialHomeomorph M H :=
+  h.isSubmersionAtOfComplement_complement.domChart
+
+/-- A choice of chart on the co-domain `N` of a submersion `f` at `x`:
+w.r.t. this chart and the data `h.domChart` and `h.equiv`,
+`f` will look like a projection `(u, v) ↦ u` in these extended charts.
+The particular chart is arbitrary, but this choice matches the witnesses given by
+`h.equiv` and `h.domChart`. -/
+def codChart (h : IsSubmersionAt I J n f x) : OpenPartialHomeomorph N G :=
+  h.isSubmersionAtOfComplement_complement.codChart
+
+lemma mem_domChart_source (h : IsSubmersionAt I J n f x) : x ∈ h.domChart.source :=
+  h.isSubmersionAtOfComplement_complement.mem_domChart_source
+
+lemma mem_codChart_source (h : IsSubmersionAt I J n f x) : f x ∈ h.codChart.source :=
+  h.isSubmersionAtOfComplement_complement.mem_codChart_source
+
+lemma domChart_mem_maximalAtlas (h : IsSubmersionAt I J n f x) :
+    h.domChart ∈ IsManifold.maximalAtlas I n M :=
+  h.isSubmersionAtOfComplement_complement.domChart_mem_maximalAtlas
+
+lemma codChart_mem_maximalAtlas (h : IsSubmersionAt I J n f x) :
+    h.codChart ∈ IsManifold.maximalAtlas J n N :=
+  h.isSubmersionAtOfComplement_complement.codChart_mem_maximalAtlas
+
+lemma source_subset_preimage_source (h : IsSubmersionAt I J n f x) :
+    h.domChart.source ⊆ f ⁻¹' h.codChart.source :=
+  h.isSubmersionAtOfComplement_complement.source_subset_preimage_source
+
+/-- A linear equivalence `E ≃L[𝕜] (E'' × F)` which belongs to the data of a submersion `f` at `x`:
+the particular equivalence is arbitrary, but this choice matches the witnesses given by
+`h.domChart` and `h.codChart`. -/
+def equiv (h : IsSubmersionAt I J n f x) : E ≃L[𝕜] (E'' × h.complement) :=
+  h.isSubmersionAtOfComplement_complement.equiv
+
+lemma writtenInCharts (h : IsSubmersionAt I J n f x) :
+    EqOn ((h.codChart.extend J) ∘ f ∘ (h.domChart.extend I).symm) (Prod.fst ∘ h.equiv)
+      (h.domChart.extend I).target :=
+  h.isSubmersionAtOfComplement_complement.writtenInCharts
+
+lemma property (h : IsSubmersionAt I J n f x) :
+    LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp h.complement I J M N) :=
+  h.isSubmersionAtOfComplement_complement.property
+
+lemma map_target_subset_target (h : IsSubmersionAt I J n f x) :
+    (Prod.fst ∘ h.equiv) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target :=
+  h.isSubmersionAtOfComplement_complement.map_target_subset_target
+
+/-- If `f` is a submersion at `x`, its domain chart's target `(h.domChart.extend I).target`
+is mapped to it codomain chart's target `(h.domChart.extend J).target`:
+see `map_target_subset_target` for a version stated using images. -/
+lemma target_subset_preimage_target (h : IsSubmersionAt I J n f x) :
+    (h.domChart.extend I).target ⊆ (Prod.fst ∘ h.equiv) ⁻¹' (h.codChart.extend J).target :=
+  fun _x hx ↦ h.map_target_subset_target (mem_image_of_mem _ hx)
+
+/-- If `f` is a submersion at `x` and `g = f` on some neighbourhood of `x`,
+then `g` is a submersion at `x`. -/
+lemma congr_of_eventuallyEq (hf : IsSubmersionAt I J n f x) (hfg : f =ᶠ[𝓝 x] g) :
+    IsSubmersionAt I J n g x := by
+  rw [IsSubmersionAt_def]
+  use hf.complement, by infer_instance, by infer_instance
+  exact hf.isSubmersionAtOfComplement_complement.congr_of_eventuallyEq hfg
+
+/-- If `f = g` on some neighbourhood of `x`,
+then `f` is a submersion at `x` if and only if `g` is an submersion at `x`. -/
+lemma congr_iff (hfg : f =ᶠ[𝓝 x] g) :
+    IsSubmersionAt I J n f x ↔ IsSubmersionAt I J n g x :=
+  ⟨fun h ↦ h.congr_of_eventuallyEq hfg, fun h ↦ h.congr_of_eventuallyEq hfg.symm⟩
+
+/- The set of points where `IsSubmersionAt` holds is open. -/
+lemma _root_.isOpen_isSubmersionAt' :
+    IsOpen {x | IsSubmersionAt I J n f x} := by
+  rw [isOpen_iff_forall_mem_open]
+  exact fun x hx ↦ ⟨{x | IsSubmersionAtOfComplement hx.complement I J n f x },
+    fun y hy ↦ hy.isSubmersionAt,
+    isOpen_isSubmersionAt, by simp [hx.isSubmersionAtOfComplement_complement]⟩
+
+/-- If `f: M → N` and `g: M' × N'` are submersions at `x` and `x'`, respectively,
+then `f × g: M × N → M' × N'` is a submersion at `(x, x')`. -/
+theorem prodMap {f : M → N} {g : M' → N'} {x' : M'}
+    [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N']
+    (hf : IsSubmersionAt I J n f x) (hg : IsSubmersionAt I' J' n g x') :
+    IsSubmersionAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x') :=
+  hf.isSubmersionAtOfComplement_complement.prodMap hg.isSubmersionAtOfComplement_complement
+    |>.isSubmersionAt
+
+end IsSubmersionAt
+
+variable (F I J n) in
+/-- `f : M → N` is a `C^k` submersion if around each point `x ∈ M`,
+there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
+such that in these charts, `f` looks like `(u, v) ↦ u`.
+
+In other words, `f` is a submersion at each `x ∈ M`.
+-/
+def IsSubmersionOfComplement (f : M → N) : Prop := ∀ x, IsSubmersionAtOfComplement F I J n f x
+
+variable (I J n) in
+/-- `f : M → N` is a `C^n` immersion if around each point `x ∈ M`,
+there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
+such that in these charts, `f` looks like `(u, v) ↦ u`.
+
+Implicit in this definition is an abstract choice `F` of a complement of `E` in `E'`:
+being a submersion includes a choice of linear isomorphism between `E` and `E'' × F`, which is where
+the choice of `F` enters. If you need stronger control over the complement `F`,
+use `IsSubmersionOfComplement` instead.
+
+Note that our global choice of complement is a bit stronger than asking `f` to be a submersion at
+each `x ∈ M` w.r.t. to potentially varying complements: see `isSubmersionAt` for details.
+-/
+def IsSubmersion (f : M → N) : Prop :=
+  ∃ (F : Type u) (_ : NormedAddCommGroup F) (_ : NormedSpace 𝕜 F),
+    IsSubmersionOfComplement F I J n f
+
+namespace IsSubmersionOfComplement
+
+variable {f g : M → N}
+
+/-- If `f` is a submersion, it is a submersion at each point. -/
+lemma isSubmersionAt (h : IsSubmersionOfComplement F I J n f) (x : M) :
+    IsSubmersionAtOfComplement F I J n f x := h x
+
+/-- If `f = g` and `f` is a submersion, so is `g`. -/
+theorem congr (h : IsSubmersionOfComplement F I J n f) (heq : f = g) :
+    IsSubmersionOfComplement F I J n g :=
+  heq ▸ h
+
+lemma trans_F (h : IsSubmersionOfComplement F I J n f) (e : F ≃L[𝕜] F') :
+    IsSubmersionOfComplement F' I J n f :=
+  fun x ↦ (h x).trans_F e
+
+/-- Being an submersion w.r.t. `F` is stable under replacing `F` by an isomorphic copy. -/
+lemma congr_F (e : F ≃L[𝕜] F') :
+    IsSubmersionOfComplement F I J n f ↔ IsSubmersionOfComplement F' I J n f :=
+  ⟨fun h ↦ trans_F (e := e) h, fun h ↦ trans_F (e := e.symm) h⟩
+
+/-- If `f: M → N` and `g: M' × N'` are submersions at `x` and `x'` (w.r.t. `F` and `F'`),
+respectively, then `f × g: M × N → M' × N'` is a submersion at `(x, x')` w.r.t. `F × F'`. -/
+theorem prodMap {f : M → N} {g : M' → N'}
+    [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N']
+    (h : IsSubmersionOfComplement F I J n f) (h' : IsSubmersionOfComplement F' I' J' n g) :
+    IsSubmersionOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g) :=
+  fun ⟨x, x'⟩ ↦ (h x).prodMap (h' x')
+
+/-- If `f` is a submersion w.r.t. some complement `F`, it is a submersion.
+
+Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe,
+while being an immersion requires the existence of a complement in the same universe as
+the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`.
+-/
+lemma isSubmersion (h : IsSubmersionOfComplement F I J n f) : IsSubmersion I J n f := by
+  by_cases! hM : IsEmpty M
+  · rw [IsSubmersion]
+    use PUnit, by infer_instance, by infer_instance
+    exact fun x ↦ (IsEmpty.false x).elim
+  inhabit M
+  let x : M := Inhabited.default
+  use (h x).smallComplement, by infer_instance, by infer_instance
+  exact (IsSubmersionOfComplement.congr_F (h x).smallEquiv).mp h
+
+end IsSubmersionOfComplement
+
+namespace IsSubmersion
+
+variable {f g : M → N}
+
+/-- A choice of complement of the model normed space `E` of `M` in the model normed space
+`E'` of `N` -/
+def complement (h : IsSubmersion I J n f) : Type u := Classical.choose h
+
+noncomputable instance (h : IsSubmersion I J n f) : NormedAddCommGroup h.complement :=
+  Classical.choose <| Classical.choose_spec h
+
+noncomputable instance (h : IsSubmersion I J n f) : NormedSpace 𝕜 h.complement :=
+  Classical.choose <| Classical.choose_spec <| Classical.choose_spec h
+
+lemma isSubmersionOfComplement_complement (h : IsSubmersion I J n f) :
+    IsSubmersionOfComplement h.complement I J n f :=
+  Classical.choose_spec <| Classical.choose_spec <| Classical.choose_spec h
+
+/-- If `f` is a submersion, it is an submersion at each point.
+-/
+lemma isImmersionAt (h : IsSubmersion I J n f) (x : M) : IsSubmersionAt I J n f x := by
+  rw [IsSubmersionAt_def]
+  use h.complement, by infer_instance, by infer_instance, h.isSubmersionOfComplement_complement x
+
+/-- If `f = g` and `f` is a submersion, so is `g`. -/
+theorem congr (h : IsSubmersion I J n f) (heq : f = g) : IsSubmersion I J n g :=
+  heq ▸ h
+
+/-- If `f: M → N` and `g: M' × N'` are submersions at `x` and `x'`, respectively,
+then `f × g: M × N → M' × N'` is an submersion at `(x, x')`. -/
+theorem prodMap {f : M → N} {g : M' → N'}
+    [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N']
+    (hf : IsSubmersion I J n f) (hg : IsSubmersion I' J' n g) :
+    IsSubmersion (I.prod I') (J.prod J') n (Prod.map f g) :=
+  (hf.isSubmersionOfComplement_complement.prodMap
+    hg.isSubmersionOfComplement_complement ).isSubmersion
+
+end IsSubmersion

From 5a3f3e5954685f0c7d270586b4b875ad41c75ed6 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Wed, 11 Feb 2026 12:03:07 +0100
Subject: [PATCH 02/18] Fix CI

---
 Mathlib.lean                              | 1 +
 Mathlib/Geometry/Manifold/Submersion.lean | 6 ++++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 71fddc4e0170b8..73e8e817a80ca7 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4344,6 +4344,7 @@ public import Mathlib.Geometry.Manifold.Sheaf.Smooth
 public import Mathlib.Geometry.Manifold.SmoothApprox
 public import Mathlib.Geometry.Manifold.SmoothEmbedding
 public import Mathlib.Geometry.Manifold.StructureGroupoid
+public import Mathlib.Geometry.Manifold.Submersion
 public import Mathlib.Geometry.Manifold.VectorBundle.Basic
 public import Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
 public import Mathlib.Geometry.Manifold.VectorBundle.Hom
diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index db98465c589249..0011c54c57fe09 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -3,7 +3,9 @@ Copyright (c) 2025 Michael Rothgang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Rothgang
 -/
-import Mathlib.Geometry.Manifold.Immersion
+module
+
+public import Mathlib.Geometry.Manifold.Immersion
 
 /-! # Smooth submersions
 
@@ -71,7 +73,7 @@ The results in this file follow from abstract results about such local propertie
 This will be the topic of Samantha Naranjo's master's thesis, and it's nice to coordinate.
 -/
 
-noncomputable section
+@[expose] public noncomputable section
 
 open scoped Topology ContDiff
 

From 5b29a7d487cb5cc325147445e4f0804ae3211036 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Wed, 11 Feb 2026 12:05:37 +0100
Subject: [PATCH 03/18] Extend documentation

---
 Mathlib/Geometry/Manifold/Submersion.lean | 28 ++++++++++++++++-------
 1 file changed, 20 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 0011c54c57fe09..682d1183b47e7f 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Michael Rothgang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Michael Rothgang
+Authors: Michael Rothgang, Samantha Naranjo Guevara
 -/
 module
 
@@ -12,14 +12,12 @@ public import Mathlib.Geometry.Manifold.Immersion
 In this file, we define `C^n` submersions between `C^n` manifolds.
 As in the case of immersions, the correct definition in the infinite-dimensional setting differs
 from the classical finite-dimensional one (which is usually phrased in terms of surjectivity of the
-`mfderiv`).
+`mfderiv`). Future work will prove that our definition implies the latter, and that both are
+equivalent for finite-dimensional manifolds.
 
-Our definition was formulated in terms of local normal forms; i.e.,
-a map `f` is a submersion at `x` if there exist charts near `x` and `f x` in which `f`
-has the standard projection `(u, v) ↦ u`, after identifying the model space of the domain with
-a product `E ≃L[𝕜] (E'' × F)`.
-
-The results in this file follow from abstract results about such local properties.
+Our definition is formulated in terms of local normal forms; i.e., a map `f` is a submersion at `x`
+if there exist charts near `x` and `f x` in which `f` looks like the standard projection
+`(u, v) ↦ u`. The results in this file follow from abstract results about such local properties.
 
 ## Main definitions
 
@@ -68,9 +66,23 @@ The results in this file follow from abstract results about such local propertie
 ## TODO
 * `IsSubmersionAt.contMDiffAt`: if f is a submersion at `x`, it is a `C^n` map at `x`.
 * `IsSubmersion.contMDiff`: if f is a submersion, it is `C^n` map.
+* If `f` is a submersion at `x`, its differential `mfderiv I J f x` admits a continuous right
+  inverse, in particular is surjective.
+* If `f : M → N` is a map between Banach manifolds, `mfderiv I J f x` having a continuous right
+  inverse implies `f` is a submersion at `x`. (This requires the inverse function theorem.)
+* `IsSubmersionAt.comp`: if `f : M → N` and `g: N → N'` are maps between Banach manifolds such that
+  `f` is a submersion at `x : M` and `g` is a submersion at `f x`, then `g ∘ f` is a submersion
+  at `x`.
+* `IsSubmersion.comp`: the composition of submersions is a submersion
+* If `f : M → N` is a map between finite-dimensional manifolds, `mfderiv I J f x` being surjective
+  implies `f` is a submersion at `x`.
+* `IsLocalDiffeomorphAt.isSubmersionAt` and `IsLocalDiffeomorph.isSubmersion`:
+  a local diffeomorphism (at `x`) is a submersion (at `x`)
+* `Diffeomorph.isSubmersion`: in particular, a diffeomorphism is a submersion
 
 **Please do not work** on this file without prior discussion with Michael Rothgang.
 This will be the topic of Samantha Naranjo's master's thesis, and it's nice to coordinate.
+
 -/
 
 @[expose] public noncomputable section

From 143933d79e33bfaaaed700123b6428356f411b43 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Wed, 11 Feb 2026 12:05:40 +0100
Subject: [PATCH 04/18] Golf a proof

---
 Mathlib/Geometry/Manifold/Submersion.lean | 29 +++++------------------
 1 file changed, 6 insertions(+), 23 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 682d1183b47e7f..7043cc7518be52 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -295,31 +295,14 @@ theorem prodMap {f : M → N} {g : M' → N'} {x' : M'}
     (hf : IsSubmersionAtOfComplement F I J n f x)
     (hg : IsSubmersionAtOfComplement F' I' J' n g x') :
     IsSubmersionAtOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x') := by
-  let P := SubmersionAtProp F I J M N
-  let Q := SubmersionAtProp F' I' J' M' N'
-  let R := SubmersionAtProp (F × F') (I.prod I') (J.prod J') (M × M') (N × N')
-  -- This is the key proof: submersions are stable under products.
-  have key : ∀ {f : M → N}, ∀ {φ₁ : OpenPartialHomeomorph M H}, ∀ {ψ₁ : OpenPartialHomeomorph N G},
-      ∀ {g : M' → N'}, ∀ {φ₂ : OpenPartialHomeomorph M' H'}, ∀ {ψ₂ : OpenPartialHomeomorph N' G'},
-      P f φ₁ ψ₁ → Q g φ₂ ψ₂ → R (Prod.map f g) (φ₁.prod φ₂) (ψ₁.prod ψ₂) := by
-    rintro f φ₁ ψ₁ g φ₂ ψ₂ ⟨equiv₁, hfprop⟩ ⟨equiv₂, hgprop⟩
-    use (equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')
-    rw [φ₁.extend_prod φ₂, ψ₁.extend_prod, PartialEquiv.prod_target]
-    set C := ((ψ₁.extend J).prod (ψ₂.extend J')) ∘
-      Prod.map f g ∘ ((φ₁.extend I).prod (φ₂.extend I')).symm
-    have hC : C = Prod.map ((ψ₁.extend J) ∘ f ∘ (φ₁.extend I).symm)
-        ((ψ₂.extend J') ∘ g ∘ (φ₂.extend I').symm) := by
-      ext x <;> simp [C]
-    set Φ := Prod.fst ∘ ((equiv₁.prodCongr equiv₂).trans
-      (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F'))
-    have hΦ: Φ = Prod.map (Prod.fst ∘ equiv₁) (Prod.fst ∘ equiv₂) := by ext x <;> simp [Φ]
-    rw [hC, hΦ]
-    exact hfprop.prodMap hgprop
   rw [IsSubmersionAtOfComplement_def]
-  exact LiftSourceTargetPropertyAt.prodMap hf.property hg.property key
+  apply LiftSourceTargetPropertyAt.prodMap hf.property hg.property
+  rintro f φ₁ ψ₁ g φ₂ ψ₂ ⟨equiv₁, hfprop⟩ ⟨equiv₂, hgprop⟩
+  use (equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')
+  rw [φ₁.extend_prod φ₂, ψ₁.extend_prod, PartialEquiv.prod_target, eqOn_prod_iff]
+  exact ⟨fun x ⟨hx, hx'⟩ ↦ by simpa using hfprop hx, fun x ⟨hx, hx'⟩ ↦ by simpa using hgprop hx'⟩
 
-/-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`.
--/
+/-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`. -/
 lemma isSubmersionAt (h : IsSubmersionAtOfComplement F I J n f x) :
     IsSubmersionAt I J n f x := by
   rw [IsSubmersionAt_def]

From 19aabd57703207f1beb191c2d83d2ee45fe9c3cd Mon Sep 17 00:00:00 2001
From: "Samantha M. Naranjo" <naranjosamantha1j@gmail.com>
Date: Wed, 11 Feb 2026 13:42:20 +0100
Subject: [PATCH 05/18] add docstrings to submersion definitions

---
 Mathlib/Geometry/Manifold/Submersion.lean | 26 +++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index db98465c589249..093aee4ca3aeb3 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -123,6 +123,18 @@ in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficien
 irreducible_def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=
   LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N)
 
+/-- `f : M → N` is a `C^k` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
+around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
+Additionally, we demand that `f` map `φ.source` into `ψ.source`.
+
+NB. We don't know the particular atlasses used for `M` and `N`, so asking for `φ` and `ψ` to be
+in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficient.
+
+Implicit in this definition is an abstract choice `F` of a complement of `E''` in `E`: being
+a submersion at `x` includes a choice of linear isomorphism between `E` and `E'' × F`, which is
+where the choice of `F` enters.
+If you need stronger control over the complement `F`, use `IsImmersionAtOfComplement` instead.
+-/
 irreducible_def IsSubmersionAt (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G)
     (n : WithTop ℕ∞) (f : M → N) (x : M) : Prop :=
   ∃ (F : Type u) (_ : NormedAddCommGroup F) (_ : NormedSpace 𝕜 F),
@@ -131,6 +143,7 @@ irreducible_def IsSubmersionAt (I : ModelWithCorners 𝕜 E H) (J : ModelWithCor
 variable {f g : M → N} {x : M}
 namespace IsSubmersionAtOfComplement
 
+#check IsImmersionAt
 lemma mk_of_charts (equiv : E ≃L[𝕜] (E'' × F)) (domChart : OpenPartialHomeomorph M H)
     (codChart : OpenPartialHomeomorph N G)
     (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source)
@@ -155,10 +168,20 @@ lemma mk_of_continuousAt {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv :
     isLocalSourceTargetProperty_submmersionAtProp
     _ _ hx hfx hdomChart hcodChart ⟨equiv, hwrittenInExtend⟩
 
+/-- A choice of chart on the domain `M` of a submersion `f` at `x`:
+w.r.t. this chart and the data `h.codChart` and `h.equiv`,
+`f` will look like a projection `(u,v) ↦ u` in these extended charts.
+The particular chart is arbitrary, but this choice matches the witnesses given by
+`h.codChart` and `h.codChart`. -/
 def domChart (h : IsSubmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph M H := by
   rw [IsSubmersionAtOfComplement_def] at h
   exact LiftSourceTargetPropertyAt.domChart h
 
+/-- A choice of chart on the codomain `N` of a submersion `f` at `x`:
+w.r.t. this chart and the data `h.domChart` and `h.equiv`,
+`f` will look like a projection `(u, v) ↦ u` in these extended charts.
+The particular chart is arbitrary, but this choice matches the witnesses given by
+`h.equiv` and `h.domChart`. -/
 def codChart (h : IsSubmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph N G := by
   rw [IsSubmersionAtOfComplement_def] at h
   exact LiftSourceTargetPropertyAt.codChart h
@@ -187,6 +210,9 @@ lemma source_subset_preimage_source (h : IsSubmersionAtOfComplement F I J n f x)
   rw [IsSubmersionAtOfComplement_def] at h
   exact LiftSourceTargetPropertyAt.source_subset_preimage_source h
 
+/-- A linear equivalence `E ≃L[𝕜] E'' × F` which belongs to the data of a submersion `f` at `x`:
+the particular equivalence is arbitrary, but this choice matches the witnesses given by
+`h.domChart` and `h.codChart`. -/
 def equiv (h : IsSubmersionAtOfComplement F I J n f x) : E ≃L[𝕜] (E'' × F) := by
   rw [IsSubmersionAtOfComplement_def] at h
   exact Classical.choose <| LiftSourceTargetPropertyAt.property h

From 529465eeec834711614ba83f4b54d7e7184e56f6 Mon Sep 17 00:00:00 2001
From: "Samantha M. Naranjo" <naranjosamantha1j@gmail.com>
Date: Wed, 11 Feb 2026 15:26:19 +0100
Subject: [PATCH 06/18] remove #check

---
 Mathlib/Geometry/Manifold/Submersion.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index cbb584c23542ce..fe583d4c02fbd3 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -157,7 +157,6 @@ irreducible_def IsSubmersionAt (I : ModelWithCorners 𝕜 E H) (J : ModelWithCor
 variable {f g : M → N} {x : M}
 namespace IsSubmersionAtOfComplement
 
-#check IsImmersionAt
 lemma mk_of_charts (equiv : E ≃L[𝕜] (E'' × F)) (domChart : OpenPartialHomeomorph M H)
     (codChart : OpenPartialHomeomorph N G)
     (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source)

From 750c454480ce0b4628090f959a3e847e6b540065 Mon Sep 17 00:00:00 2001
From: "Samantha M. Naranjo" <naranjosamantha1j@gmail.com>
Date: Thu, 26 Mar 2026 09:45:50 +0100
Subject: [PATCH 07/18] Remove immersions

---
 Mathlib/Geometry/Manifold/Submersion.lean | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index fe583d4c02fbd3..4c522524b43cfb 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -5,7 +5,10 @@ Authors: Michael Rothgang, Samantha Naranjo Guevara
 -/
 module
 
-public import Mathlib.Geometry.Manifold.Immersion
+public import Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
+public import Mathlib.Geometry.Manifold.LocalSourceTargetProperty
+public import Mathlib.Analysis.Normed.Module.Shrink
+public import Mathlib.Topology.Algebra.Module.TransferInstance
 
 /-! # Smooth submersions
 
@@ -59,9 +62,9 @@ if there exist charts near `x` and `f x` in which `f` looks like the standard pr
 * To avoid a free universe variable in `IsSubmersion(At)`, we require the complement to be taken in
   the same universe as the model normed space for `N`. We also offer convenience constructors that
   relax this requirement to preserve usability. This relies on the observation that the equivalence
-  in the definition of immersions allows the universe of the complement to be reduced,
-  as implemented in `IsImmersion(At)OfComplement.small`
-  and  `IsImmersion(At)OfComplement.smallEquiv`.
+  in the definition of submersions allows the universe of the complement to be reduced,
+  as implemented in `IsSubmersion(At)OfComplement.small`
+  and  `IsSubmersion(At)OfComplement.smallEquiv`.
 
 ## TODO
 * `IsSubmersionAt.contMDiffAt`: if f is a submersion at `x`, it is a `C^n` map at `x`.
@@ -147,7 +150,7 @@ in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficien
 Implicit in this definition is an abstract choice `F` of a complement of `E''` in `E`: being
 a submersion at `x` includes a choice of linear isomorphism between `E` and `E'' × F`, which is
 where the choice of `F` enters.
-If you need stronger control over the complement `F`, use `IsImmersionAtOfComplement` instead.
+If you need stronger control over the complement `F`, use `IsSubmersionAtOfComplement` instead.
 -/
 irreducible_def IsSubmersionAt (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G)
     (n : WithTop ℕ∞) (f : M → N) (x : M) : Prop :=
@@ -327,7 +330,7 @@ theorem prodMap {f : M → N} {g : M' → N'} {x' : M'}
   rw [φ₁.extend_prod φ₂, ψ₁.extend_prod, PartialEquiv.prod_target, eqOn_prod_iff]
   exact ⟨fun x ⟨hx, hx'⟩ ↦ by simpa using hfprop hx, fun x ⟨hx, hx'⟩ ↦ by simpa using hgprop hx'⟩
 
-/-- If `f` is an immersion at `x` w.r.t. some complement `F`, it is an immersion at `x`. -/
+/-- If `f` is an submersion at `x` w.r.t. some complement `F`, it is an submersion at `x`. -/
 lemma isSubmersionAt (h : IsSubmersionAtOfComplement F I J n f x) :
     IsSubmersionAt I J n f x := by
   rw [IsSubmersionAt_def]
@@ -491,7 +494,7 @@ In other words, `f` is a submersion at each `x ∈ M`.
 def IsSubmersionOfComplement (f : M → N) : Prop := ∀ x, IsSubmersionAtOfComplement F I J n f x
 
 variable (I J n) in
-/-- `f : M → N` is a `C^n` immersion if around each point `x ∈ M`,
+/-- `f : M → N` is a `C^n` submersion if around each point `x ∈ M`,
 there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
 such that in these charts, `f` looks like `(u, v) ↦ u`.
 
@@ -540,7 +543,7 @@ theorem prodMap {f : M → N} {g : M' → N'}
 /-- If `f` is a submersion w.r.t. some complement `F`, it is a submersion.
 
 Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe,
-while being an immersion requires the existence of a complement in the same universe as
+while being an submersion requires the existence of a complement in the same universe as
 the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`.
 -/
 lemma isSubmersion (h : IsSubmersionOfComplement F I J n f) : IsSubmersion I J n f := by
@@ -575,7 +578,7 @@ lemma isSubmersionOfComplement_complement (h : IsSubmersion I J n f) :
 
 /-- If `f` is a submersion, it is an submersion at each point.
 -/
-lemma isImmersionAt (h : IsSubmersion I J n f) (x : M) : IsSubmersionAt I J n f x := by
+lemma isSubmersionAt (h : IsSubmersion I J n f) (x : M) : IsSubmersionAt I J n f x := by
   rw [IsSubmersionAt_def]
   use h.complement, by infer_instance, by infer_instance, h.isSubmersionOfComplement_complement x
 

From 798e0cbee12ee3a1ee56039e0ab4d9d4a89d986f Mon Sep 17 00:00:00 2001
From: "Samantha M. Naranjo" <naranjosamantha1j@gmail.com>
Date: Thu, 16 Apr 2026 10:57:58 +0200
Subject: [PATCH 08/18] tranparency

---
 Mathlib/Geometry/Manifold/Submersion.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 4c522524b43cfb..d0cbe651d71549 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -282,6 +282,7 @@ instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.s
   unfold smallComplement
   infer_instance
 
+set_option backward.isDefEq.respectTransparency false in
 instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement := by
   haveI := hf.small
   unfold smallComplement
@@ -316,6 +317,7 @@ lemma _root_.isOpen_isSubmersionAt :
   simp_rw [IsSubmersionAtOfComplement_def]
   exact IsOpen.liftSourceTargetPropertyAt
 
+set_option backward.isDefEq.respectTransparency false in
 /-- If `f: M → N` and `g: M' × N'` are submersions at `x` and `x'`, respectively,
 then `f × g: M × N → M' × N'` is an submersion at `(x, x')`. -/
 theorem prodMap {f : M → N} {g : M' → N'} {x' : M'}

From db60057306fa1d91c92dfad943168520fdcb1a22 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Fri, 17 Apr 2026 15:20:24 +0200
Subject: [PATCH 09/18] chore: wording tweaks for immersion module doc-string

---
 Mathlib/Geometry/Manifold/Immersion.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean
index 412daefb42e3c3..ab894c3199ead3 100644
--- a/Mathlib/Geometry/Manifold/Immersion.lean
+++ b/Mathlib/Geometry/Manifold/Immersion.lean
@@ -43,27 +43,27 @@ This shortens the overall argument, as the definition of submersions has the sam
   If `f` and `g` agree near `x` and `f` is an immersion at `x`, so is `g`
 * `IsImmersionAtOfComplement.congr_F`, `IsImmersionOfComplement.congr_F`:
   being an immersion (at `x`) w.r.t. `F` is stable under
-  replacing the complement `F` by an isomorphic copy
+  replacing the complement `F` by an isomorphic copy.
 * `IsOpen.isImmersionAtOfComplement` and `IsOpen.isImmersionAt`:
   the set of points where `IsImmersionAt(OfComplement)` holds is open.
 * `IsImmersionAt.prodMap` and `IsImmersion.prodMap`: the product of two immersions (at a point)
-  is an immersion (at a point).
+  is an immersion (at the product point).
 * `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
 
 ## Implementation notes
 
-* In most applications, there is no need to control the chosen complement in the definition of
-  immersions, so `IsImmersion(At)` is perfectly fine to use. Such control will be helpful, however,
+* In most applications, there is no need to control the choice of complement in the definition of an
+  immersion, so `IsImmersion(At)` is perfectly adequate. Such control will be helpful, however,
   when considering the local characterisation of submanifolds: locally, a submanifold is described
   either as the image of an immersion, or the preimage of a submersion --- w.r.t. the same
-  complement. Having access to a definition version with complements allows stating this equivalence
-  cleanly.
+  complement. Providing a version of the definition that includes complements enables stating this
+  equivalence cleanly.
 * To avoid a free universe variable in `IsImmersion(At)`, we ask for a complement in the same
   universe as the model normed space for `N`. We provide convenience constructors which do not
-  have this restriction (recovering usability).
-  The underlying observation is that the equivalence in the definition of immersions allows
+  have this restriction to preserve usability.
+  This relies on the observation that the equivalence in the definition of immersions allows
   shrinking the universe of the complement: this is implemented in
   `IsImmersion(At)OfComplement.small` and `IsImmersion(At)OfComplement.smallEquiv`.
 

From 84f810d96adb69b1af4f262fa1efc91ba6199ca9 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Fri, 17 Apr 2026 15:20:46 +0200
Subject: [PATCH 10/18] chore: tweak module doc-string

---
 Mathlib/Geometry/Manifold/Submersion.lean | 36 +++++++++++------------
 1 file changed, 17 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index d0cbe651d71549..8a214423697310 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -41,34 +41,32 @@ if there exist charts near `x` and `f x` in which `f` looks like the standard pr
   If `f` and `g` agree near `x` and `f` is a submersion at `x`, then so is `g`.
 * `IsSubmersionAtOfComplement.congr_F`, `IsSubmersionOfComplement.congr_F`:
   being a submersion at `x` w.r.t. `F` is stable under
-  replacing the complement `F` by a continuously linearly equivalent copy of `F`.
+  replacing the complement `F` by an isomorphic copy.
 * `isOpen_isSubmersionAtOfComplement` and `isOpen_isSubmersionAt`:
   the set of points where `IsSubmersionAt(OfComplement)` holds is open.
-* `IsSubmersionAt.prodMap` and `IsSubmersion.prodMap`: the product of two submersions at a point
-  is an submersion at the product point.
+* `IsSubmersionAt.prodMap` and `IsSubmersion.prodMap`: the product of two submersions (at a point)
+  is an submersion (at the product point).
 
 ## Implementation notes
 
-* Universe management tools (`small`, `smallComplement`, `smallEquiv`) ensure that
-  complements can always be chosen in the correct universe, which is essential for
-  existential definitions such as `isSubmersionAt`.
 * In most applications, there is no need to control the choice of complement in the definition of a
   submersion, so `IsSubmersion(At)` is perfectly adequate. Nevertheless, explicit control over
-  complements becomes useful when studying the local characterisation of submanifolds. Locally,
-  a submanifold can be described either as the image of a submersion or as the preimage of
-  an immersion, and this equivalence requires working with the same choice of complement.
-  Providing a version of the definition that includes complements allows this equivalence to be
-  stated cleanly.
-* To avoid a free universe variable in `IsSubmersion(At)`, we require the complement to be taken in
-  the same universe as the model normed space for `N`. We also offer convenience constructors that
-  relax this requirement to preserve usability. This relies on the observation that the equivalence
-  in the definition of submersions allows the universe of the complement to be reduced,
-  as implemented in `IsSubmersion(At)OfComplement.small`
-  and  `IsSubmersion(At)OfComplement.smallEquiv`.
+  complements is useful when studying the local characterisation of submanifolds: locally,
+  a submanifold is described either as the image of an immersion, or the preimage of a submersion
+  --- w.r.t. the same complement. Providing a version of the definition that includes complements
+  enables stating this equivalence cleanly.
+* To avoid a free universe variable in `IsSubmersion(At)`, we ask for a complement in the same
+  universe as the model normed space for `N`. We provide convenience constructors which do not
+  have this restriction to preserve usability.
+  This relies on the observation that the equivalence in the definition of submersions allows
+  reducing the universe of the complement; this is implemented in
+  `IsSubmersion(At)OfComplement.small` and  `IsSubmersion(At)OfComplement.smallEquiv`.
 
 ## TODO
-* `IsSubmersionAt.contMDiffAt`: if f is a submersion at `x`, it is a `C^n` map at `x`.
-* `IsSubmersion.contMDiff`: if f is a submersion, it is `C^n` map.
+* The converse to `IsSubmersionAtOfComplement.congr_F` also holds: any two complements are
+  isomorphic, as they are isomorphic to the kernel of the differential `mfderiv I J f x`.
+* `IsSubmersionAt.contMDiffAt`: if f is a submersion at `x`, it is `C^n` at `x`.
+* `IsSubmersion.contMDiff`: if f is a submersion, it is `C^n`.
 * If `f` is a submersion at `x`, its differential `mfderiv I J f x` admits a continuous right
   inverse, in particular is surjective.
 * If `f : M → N` is a map between Banach manifolds, `mfderiv I J f x` having a continuous right

From 0be990fa52c2928bf8c0223d94f88a62e2a47199 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Fri, 17 Apr 2026 16:09:19 +0200
Subject: [PATCH 11/18] chore: fix one use of
 backward.isDefEq.respectTransparency option

---
 Mathlib/Geometry/Manifold/Submersion.lean | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 8a214423697310..cc7b4b1a66e66d 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -275,16 +275,13 @@ def smallComplement (hf : IsSubmersionAtOfComplement F I J n f x) : Type u :=
   haveI := hf.small
   Shrink.{u} F
 
-instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement := by
+instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedAddCommGroup hf.smallComplement :=
   haveI := hf.small
-  unfold smallComplement
-  infer_instance
+  inferInstanceAs <| NormedAddCommGroup (Shrink F)
 
-set_option backward.isDefEq.respectTransparency false in
-instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement := by
+instance (hf : IsSubmersionAtOfComplement F I J n f x) : NormedSpace 𝕜 hf.smallComplement :=
   haveI := hf.small
-  unfold smallComplement
-  infer_instance
+  inferInstanceAs <| NormedSpace 𝕜 (Shrink F)
 
 /-- Given an submersion `f` at `x` w.r.t. a complement `F`, this construction provides
 a continuous linear equivalence from `F` to the small complement of `F`:

From 9f85b775f029c10455904ed78df5335c9f5e4763 Mon Sep 17 00:00:00 2001
From: "Samantha M. Naranjo" <naranjosamantha1j@gmail.com>
Date: Thu, 30 Apr 2026 13:08:25 +0200
Subject: [PATCH 12/18] some corrections

---
 Mathlib/Geometry/Manifold/Submersion.lean | 47 +++++++++++++++--------
 1 file changed, 31 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index cc7b4b1a66e66d..535dd5ac63ec0a 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -29,7 +29,7 @@ if there exist charts near `x` and `f x` in which `f` looks like the standard pr
   respectively, such that in these charts, `f` looks like `(u, v) ↦ u`, w.r.t. some equivalence
   `E ≃L[𝕜] (E'' × F)`. Differentiability of `f` is not assumed as it follows from this definition.
 * `IsSubmersionAt I J n f x` means that `f` is a `C^n` submersion at `x : M` for some choice of a
-  complement `F` of the model normed space `E` of `M` in the model normed space `E'` of `N`.
+  complement `F` of the model normed space `E` of `M` in the model normed space `E''` of `N`.
 * `IsSubmersionOfComplement F I J n f` means `f : M → N` is a submersion at every point `x : M`,
   w.r.t. the chosen complement `F`.
 * `IsSubmersion I J n f` means `f : M → N` is a submersion at every point `x : M`,
@@ -90,9 +90,12 @@ This will be the topic of Samantha Naranjo's master's thesis, and it's nice to c
 
 open scoped Topology ContDiff
 
-open Function Set Manifold
+open Function Set
+
+namespace Manifold
 
 universe u
+-- We manually name the universe of `E` as `IsSubmersionAt` will use it.
 
 variable {𝕜 E' E'' E''' F F' H H' G G' : Type*} {E : Type u} [NontriviallyNormedField 𝕜]
   [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
@@ -108,11 +111,15 @@ variable {M M' N N' : Type*}
   {n : WithTop ℕ∞}
 
 variable (F I J M N) in
-/-- The local property of being a submersion at `x` -/
+/-- The local property of being a submersion at a point: `f : M → N` is a submersion at `x` if
+there exist charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively, such that in these
+charts, `f` looks like the projection `(u, v) ↦ u`.
+This definition has a fixed parameter `F`, which is a choice of complement of `E''` in the model
+normed space `E` of `M`: being a submersion at `x` includes a choice of linear isomorphism
+between `E'' × F` and `E`. -/
 def SubmersionAtProp :
-    ((M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop) :=
-  fun f domChart codChart ↦
-    ∃ equiv : E ≃L[𝕜] (E'' × F),
+    (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop :=
+  fun f domChart codChart ↦ ∃ equiv : E ≃L[𝕜] (E'' × F),
     EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
       (domChart.extend I).target
 
@@ -121,24 +128,31 @@ omit [ChartedSpace H M] [ChartedSpace G N] in
 lemma isLocalSourceTargetProperty_submmersionAtProp :
     IsLocalSourceTargetProperty (SubmersionAtProp F I J M N) where
   mono_source {f φ ψ s} hs := fun ⟨equiv, hf⟩ ↦ ⟨equiv, hf.mono (by simp; grind)⟩
-  congr {f g φ ψ} hfg hf := by
-    obtain ⟨equiv, hf⟩ := hf
+  congr {f g φ ψ} hfg := by
+    intro ⟨equiv, hf⟩
     refine ⟨equiv, EqOn.trans (fun x hx ↦ ?_) (hf.mono (by simp))⟩
     have : ((φ.extend I).symm) x ∈ φ.source := by simp_all
     grind
 
 variable (F I J n) in
-/-- `f : M → N` is a `C^k` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
+/-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
 around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
 Additionally, we demand that `f` map `φ.source` into `ψ.source`.
 
 NB. We don't know the particular atlasses used for `M` and `N`, so asking for `φ` and `ψ` to be
 in the `atlas` would be too optimistic: lying in the `maximalAtlas` is sufficient.
+
+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`.
+While the particular choice of complement is often not important, choosing a complement is useful
+in some settings, such as proving that embedded submanifolds are locally given either by an
+immersion or a submersion.
+Unless you have a particular reason, prefer to use `IsSubmersionAt` instead.
 -/
 irreducible_def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=
   LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N)
-
-/-- `f : M → N` is a `C^k` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
+variable (I J n) in
+/-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
 around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
 Additionally, we demand that `f` map `φ.source` into `ψ.source`.
 
@@ -156,6 +170,7 @@ irreducible_def IsSubmersionAt (I : ModelWithCorners 𝕜 E H) (J : ModelWithCor
     IsSubmersionAtOfComplement F I J n f x
 
 variable {f g : M → N} {x : M}
+
 namespace IsSubmersionAtOfComplement
 
 lemma mk_of_charts (equiv : E ≃L[𝕜] (E'' × F)) (domChart : OpenPartialHomeomorph M H)
@@ -375,11 +390,11 @@ def complement (h : IsSubmersionAt I J n f x) : Type u := by
   rw [IsSubmersionAt_def] at h
   exact Classical.choose h
 
-noncomputable instance (h : IsSubmersionAt I J n f x) : NormedAddCommGroup h.complement := by
+instance (h : IsSubmersionAt I J n f x) : NormedAddCommGroup h.complement := by
   rw [IsSubmersionAt_def] at h
   exact Classical.choose <| Classical.choose_spec h
 
-noncomputable instance (h : IsSubmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by
+instance (h : IsSubmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by
   rw [IsSubmersionAt_def] at h
   exact Classical.choose <| Classical.choose_spec <| Classical.choose_spec h
 
@@ -482,7 +497,7 @@ theorem prodMap {f : M → N} {g : M' → N'} {x' : M'}
 end IsSubmersionAt
 
 variable (F I J n) in
-/-- `f : M → N` is a `C^k` submersion if around each point `x ∈ M`,
+/-- `f : M → N` is a `C^n` submersion if around each point `x ∈ M`,
 there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
 such that in these charts, `f` looks like `(u, v) ↦ u`.
 
@@ -563,10 +578,10 @@ variable {f g : M → N}
 `E'` of `N` -/
 def complement (h : IsSubmersion I J n f) : Type u := Classical.choose h
 
-noncomputable instance (h : IsSubmersion I J n f) : NormedAddCommGroup h.complement :=
+instance (h : IsSubmersion I J n f) : NormedAddCommGroup h.complement :=
   Classical.choose <| Classical.choose_spec h
 
-noncomputable instance (h : IsSubmersion I J n f) : NormedSpace 𝕜 h.complement :=
+instance (h : IsSubmersion I J n f) : NormedSpace 𝕜 h.complement :=
   Classical.choose <| Classical.choose_spec <| Classical.choose_spec h
 
 lemma isSubmersionOfComplement_complement (h : IsSubmersion I J n f) :

From 84c649fddf83123b12e9c3168280fed73aa48e44 Mon Sep 17 00:00:00 2001
From: "Samantha M. Naranjo" <naranjosamantha1j@gmail.com>
Date: Mon, 4 May 2026 14:34:10 +0200
Subject: [PATCH 13/18] doc-strings and other minor tweaks

---
 Mathlib/Geometry/Manifold/Submersion.lean | 51 +++++++++++++++++++++--
 1 file changed, 47 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 535dd5ac63ec0a..11f0e022a595c0 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -151,6 +151,7 @@ Unless you have a particular reason, prefer to use `IsSubmersionAt` instead.
 -/
 irreducible_def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=
   LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N)
+
 variable (I J n) in
 /-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
 around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.
@@ -164,8 +165,7 @@ a submersion at `x` includes a choice of linear isomorphism between `E` and `E''
 where the choice of `F` enters.
 If you need stronger control over the complement `F`, use `IsSubmersionAtOfComplement` instead.
 -/
-irreducible_def IsSubmersionAt (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 E'' G)
-    (n : WithTop ℕ∞) (f : M → N) (x : M) : Prop :=
+irreducible_def IsSubmersionAt (f : M → N) (x : M) : Prop :=
   ∃ (F : Type u) (_ : NormedAddCommGroup F) (_ : NormedSpace 𝕜 F),
     IsSubmersionAtOfComplement F I J n f x
 
@@ -185,6 +185,10 @@ lemma mk_of_charts (equiv : E ≃L[𝕜] (E'' × F)) (domChart : OpenPartialHome
   use domChart, codChart
   use equiv
 
+/-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
+around `x` and `f x`, respectively such that in these charts, `f` looks like `(u,v) ↦ u`.
+This version does not assume that `f` maps `φ.source` to `ψ.source`,
+but that `f` is continuous at `x`. -/
 lemma mk_of_continuousAt {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv : E ≃L[𝕜] (E'' × F))
     (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G)
     (hx : x ∈ domChart.source) (hfx : f x ∈ codChart.source)
@@ -256,6 +260,11 @@ lemma property (h : IsSubmersionAtOfComplement F I J n f x) :
     LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N) := by
   rwa [IsSubmersionAtOfComplement_def] at h
 
+/-- If `f` is a submersion at `x`, it maps its domain chart's target to its codomain chart's target:
+`(h.domChart.extend I).target` to `(h.domChart.extend J).target`.
+
+See `target_subset_preimage_target` for a version stated using preimages instead of images.
+-/
 lemma map_target_subset_target (h : IsSubmersionAtOfComplement F I J n f x) :
     (Prod.fst ∘ h.equiv) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target := by
   rw [← h.writtenInCharts.image_eq, Set.image_comp, Set.image_comp,
@@ -265,16 +274,23 @@ lemma map_target_subset_target (h : IsSubmersionAtOfComplement F I J n f x) :
     simp [h.source_subset_preimage_source]
   grw [this, OpenPartialHomeomorph.extend_source]
 
+/-- If `f` is a submersion at `x`, its domain chart's target `(h.domChart.extend I).target`
+is mapped to its codomain chart's target `(h.domChart.extend J).target`:
+see `map_target_subset_target` for a version stated using images. -/
 lemma target_subset_preimage_target (h : IsSubmersionAtOfComplement F I J n f x) :
     (h.domChart.extend I).target ⊆ (Prod.fst ∘ h.equiv) ⁻¹' (h.codChart.extend J).target :=
   fun _x hx ↦ h.map_target_subset_target (mem_image_of_mem _ hx)
 
+/-- If `f` is a submersion at `x` and `g = f` on some neighbourhood of `x`,
+then `g` is a submersion at `x`. -/
 lemma congr_of_eventuallyEq (hf : IsSubmersionAtOfComplement F I J n f x) (hfg : f =ᶠ[𝓝 x] g) :
     IsSubmersionAtOfComplement F I J n g x := by
   rw [IsSubmersionAtOfComplement_def]
   exact LiftSourceTargetPropertyAt.congr_of_eventuallyEq
     isLocalSourceTargetProperty_submmersionAtProp hf.property hfg
 
+/-- If `f = g` on some neighbourhood of `x`,
+then `f` is a submersion at `x` if and only if `g` is a submersion at `x`. -/
 lemma congr_iff_of_eventuallyEq (hfg : f =ᶠ[𝓝 x] g) :
     IsSubmersionAtOfComplement F I J n f x ↔ IsSubmersionAtOfComplement F I J n g x := by
   simpa only [IsSubmersionAtOfComplement_def] using
@@ -342,7 +358,11 @@ theorem prodMap {f : M → N} {g : M' → N'} {x' : M'}
   rw [φ₁.extend_prod φ₂, ψ₁.extend_prod, PartialEquiv.prod_target, eqOn_prod_iff]
   exact ⟨fun x ⟨hx, hx'⟩ ↦ by simpa using hfprop hx, fun x ⟨hx, hx'⟩ ↦ by simpa using hgprop hx'⟩
 
-/-- If `f` is an submersion at `x` w.r.t. some complement `F`, it is an submersion at `x`. -/
+/-- If `f` is a submersion at `x` w.r.t. some complement `F`, it is an submersion at `x`.
+
+Note that the proof contains a small formalisation-related subtlety: `F` can live in any universe,
+while being a submersion at `x` requires the existence of a complement in the same universe as
+the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`. -/
 lemma isSubmersionAt (h : IsSubmersionAtOfComplement F I J n f x) :
     IsSubmersionAt I J n f x := by
   rw [IsSubmersionAt_def]
@@ -452,6 +472,8 @@ lemma property (h : IsSubmersionAt I J n f x) :
     LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp h.complement I J M N) :=
   h.isSubmersionAtOfComplement_complement.property
 
+/-- If `f` is a submersion at `x`, it maps its domain chart's target to its codomain chart's target:
+`(h.domChart.extend I).target` to `(h.domChart.extend J).target`. -/
 lemma map_target_subset_target (h : IsSubmersionAt I J n f x) :
     (Prod.fst ∘ h.equiv) '' (h.domChart.extend I).target ⊆ (h.codChart.extend J).target :=
   h.isSubmersionAtOfComplement_complement.map_target_subset_target
@@ -502,7 +524,9 @@ there are charts `φ` and `ψ` of `M` and `N` around `x` and `f x`, respectively
 such that in these charts, `f` looks like `(u, v) ↦ u`.
 
 In other words, `f` is a submersion at each `x ∈ M`.
--/
+
+This definition has a fixed parameter `F`, which is a choice of complement of `E` in `E'`:
+being an submersion at `x` includes a choice of linear isomorphism between `E` and `E'' × F`. -/
 def IsSubmersionOfComplement (f : M → N) : Prop := ∀ x, IsSubmersionAtOfComplement F I J n f x
 
 variable (I J n) in
@@ -568,6 +592,19 @@ lemma isSubmersion (h : IsSubmersionOfComplement F I J n f) : IsSubmersion I J n
   use (h x).smallComplement, by infer_instance, by infer_instance
   exact (IsSubmersionOfComplement.congr_F (h x).smallEquiv).mp h
 
+open IsManifold in
+/-- The identity map is a submersion with complement `PUnit`. -/
+protected lemma id [IsManifold I n M] : IsSubmersionOfComplement PUnit I I n (@id M) := by
+  intro x
+  apply IsSubmersionAtOfComplement.mk_of_continuousAt (continuousAt_id)
+    (ContinuousLinearEquiv.prodUnique 𝕜 E PUnit).symm
+    (chartAt H x) (chartAt H x) (mem_chart_source H x) (mem_chart_source H x)
+    (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas 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
+
 end IsSubmersionOfComplement
 
 namespace IsSubmersion
@@ -607,4 +644,10 @@ theorem prodMap {f : M → N} {g : M' → N'}
   (hf.isSubmersionOfComplement_complement.prodMap
     hg.isSubmersionOfComplement_complement ).isSubmersion
 
+/-- The identity map is an submersion. -/
+protected lemma id [IsManifold I n M] : IsSubmersion I I n (@id M) :=
+  ⟨PUnit, by infer_instance, by infer_instance, IsSubmersionOfComplement.id⟩
+
 end IsSubmersion
+
+end Manifold

From 50d9d45e8d21f9e05d83c6e631899e4001e52a5c Mon Sep 17 00:00:00 2001
From: "Samantha M. Naranjo" <naranjosamantha1j@gmail.com>
Date: Mon, 4 May 2026 15:16:18 +0200
Subject: [PATCH 14/18] comment

---
 Mathlib/Geometry/Manifold/Submersion.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 11f0e022a595c0..1a5a7ba5f1a496 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -152,6 +152,8 @@ Unless you have a particular reason, prefer to use `IsSubmersionAt` instead.
 irreducible_def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=
   LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N)
 
+-- Lift the universe from `E`, to avoid a free universe parameter.
+
 variable (I J n) in
 /-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
 around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.

From 62bc8fc9967cea7edb8728b5ae6cb517f838f3f8 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Wed, 6 May 2026 10:43:16 +0200
Subject: [PATCH 15/18] Superfluous newline

---
 Mathlib/Geometry/Manifold/Submersion.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 1a5a7ba5f1a496..64f0dc4997df13 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -153,7 +153,6 @@ irreducible_def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=
   LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N)
 
 -- Lift the universe from `E`, to avoid a free universe parameter.
-
 variable (I J n) in
 /-- `f : M → N` is a `C^n` submersion at `x` if there are charts `φ` and `ψ` of `M` and `N`
 around `x` and `f x`, respectively such that in these charts, `f` looks like `(u, v) ↦ u`.

From 6cb582047bfd0ed370ce1aad2376a6352a88ce5f Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Wed, 6 May 2026 15:20:22 +0200
Subject: [PATCH 16/18] chore: use no_expose instead

---
 Mathlib/Geometry/Manifold/Submersion.lean | 76 +++++++++--------------
 1 file changed, 31 insertions(+), 45 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 64f0dc4997df13..ff03d7b09bdf07 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -149,7 +149,7 @@ in some settings, such as proving that embedded submanifolds are locally given e
 immersion or a submersion.
 Unless you have a particular reason, prefer to use `IsSubmersionAt` instead.
 -/
-irreducible_def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=
+@[no_expose] def IsSubmersionAtOfComplement (f : M → N) (x : M) : Prop :=
   LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N)
 
 -- Lift the universe from `E`, to avoid a free universe parameter.
@@ -182,7 +182,6 @@ lemma mk_of_charts (equiv : E ≃L[𝕜] (E'' × F)) (domChart : OpenPartialHome
     (hsource : domChart.source ⊆ f ⁻¹' codChart.source)
     (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
       (domChart.extend I).target) : IsSubmersionAtOfComplement F I J n f x := by
-  rw [IsSubmersionAtOfComplement_def]
   use domChart, codChart
   use equiv
 
@@ -197,7 +196,6 @@ lemma mk_of_continuousAt {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv :
     (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N)
     (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
       (domChart.extend I).target) : IsSubmersionAtOfComplement F I J n f x := by
-  rw [IsSubmersionAtOfComplement_def]
   exact LiftSourceTargetPropertyAt.mk_of_continuousAt hf
     isLocalSourceTargetProperty_submmersionAtProp
     _ _ hx hfx hdomChart hcodChart ⟨equiv, hwrittenInExtend⟩
@@ -207,59 +205,50 @@ w.r.t. this chart and the data `h.codChart` and `h.equiv`,
 `f` will look like a projection `(u,v) ↦ u` in these extended charts.
 The particular chart is arbitrary, but this choice matches the witnesses given by
 `h.codChart` and `h.codChart`. -/
-def domChart (h : IsSubmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph M H := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact LiftSourceTargetPropertyAt.domChart h
+@[no_expose] def domChart (h : IsSubmersionAtOfComplement F I J n f x) :
+    OpenPartialHomeomorph M H :=
+  LiftSourceTargetPropertyAt.domChart h
 
 /-- A choice of chart on the codomain `N` of a submersion `f` at `x`:
 w.r.t. this chart and the data `h.domChart` and `h.equiv`,
 `f` will look like a projection `(u, v) ↦ u` in these extended charts.
 The particular chart is arbitrary, but this choice matches the witnesses given by
 `h.equiv` and `h.domChart`. -/
-def codChart (h : IsSubmersionAtOfComplement F I J n f x) : OpenPartialHomeomorph N G := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact LiftSourceTargetPropertyAt.codChart h
+@[no_expose] def codChart (h : IsSubmersionAtOfComplement F I J n f x) :
+    OpenPartialHomeomorph N G :=
+  LiftSourceTargetPropertyAt.codChart h
 
-lemma mem_domChart_source (h : IsSubmersionAtOfComplement F I J n f x) : x ∈ h.domChart.source := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact LiftSourceTargetPropertyAt.mem_domChart_source h
+lemma mem_domChart_source (h : IsSubmersionAtOfComplement F I J n f x) : x ∈ h.domChart.source :=
+  LiftSourceTargetPropertyAt.mem_domChart_source h
 
-lemma mem_codChart_source (h : IsSubmersionAtOfComplement F I J n f x) :
-    f x ∈ h.codChart.source := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact LiftSourceTargetPropertyAt.mem_codChart_source h
+lemma mem_codChart_source (h : IsSubmersionAtOfComplement F I J n f x) : f x ∈ h.codChart.source :=
+  LiftSourceTargetPropertyAt.mem_codChart_source h
 
 lemma domChart_mem_maximalAtlas (h : IsSubmersionAtOfComplement F I J n f x) :
-    h.domChart ∈ IsManifold.maximalAtlas I n M := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas h
+    h.domChart ∈ IsManifold.maximalAtlas I n M :=
+  LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas h
 
 lemma codChart_mem_maximalAtlas (h : IsSubmersionAtOfComplement F I J n f x) :
-    h.codChart ∈ IsManifold.maximalAtlas J n N := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas h
+    h.codChart ∈ IsManifold.maximalAtlas J n N :=
+  LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas h
 
 lemma source_subset_preimage_source (h : IsSubmersionAtOfComplement F I J n f x) :
-    h.domChart.source ⊆ f ⁻¹' h.codChart.source := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact LiftSourceTargetPropertyAt.source_subset_preimage_source h
+    h.domChart.source ⊆ f ⁻¹' h.codChart.source :=
+  LiftSourceTargetPropertyAt.source_subset_preimage_source h
 
 /-- A linear equivalence `E ≃L[𝕜] E'' × F` which belongs to the data of a submersion `f` at `x`:
 the particular equivalence is arbitrary, but this choice matches the witnesses given by
 `h.domChart` and `h.codChart`. -/
-def equiv (h : IsSubmersionAtOfComplement F I J n f x) : E ≃L[𝕜] (E'' × F) := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact Classical.choose <| LiftSourceTargetPropertyAt.property h
+@[no_expose] def equiv (h : IsSubmersionAtOfComplement F I J n f x) : E ≃L[𝕜] (E'' × F) :=
+  Classical.choose <| LiftSourceTargetPropertyAt.property h
 
 lemma writtenInCharts (h : IsSubmersionAtOfComplement F I J n f x) :
     EqOn ((h.codChart.extend J) ∘ f ∘ (h.domChart.extend I).symm) (Prod.fst ∘ h.equiv)
-      (h.domChart.extend I).target := by
-  rw [IsSubmersionAtOfComplement_def] at h
-  exact Classical.choose_spec <| LiftSourceTargetPropertyAt.property h
+      (h.domChart.extend I).target :=
+  Classical.choose_spec <| LiftSourceTargetPropertyAt.property h
 
 lemma property (h : IsSubmersionAtOfComplement F I J n f x) :
-    LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N) := by
-  rwa [IsSubmersionAtOfComplement_def] at h
+    LiftSourceTargetPropertyAt I J n f x (SubmersionAtProp F I J M N) := h
 
 /-- If `f` is a submersion at `x`, it maps its domain chart's target to its codomain chart's target:
 `(h.domChart.extend I).target` to `(h.domChart.extend J).target`.
@@ -286,17 +275,15 @@ lemma target_subset_preimage_target (h : IsSubmersionAtOfComplement F I J n f x)
 then `g` is a submersion at `x`. -/
 lemma congr_of_eventuallyEq (hf : IsSubmersionAtOfComplement F I J n f x) (hfg : f =ᶠ[𝓝 x] g) :
     IsSubmersionAtOfComplement F I J n g x := by
-  rw [IsSubmersionAtOfComplement_def]
   exact LiftSourceTargetPropertyAt.congr_of_eventuallyEq
     isLocalSourceTargetProperty_submmersionAtProp hf.property hfg
 
 /-- If `f = g` on some neighbourhood of `x`,
 then `f` is a submersion at `x` if and only if `g` is a submersion at `x`. -/
 lemma congr_iff_of_eventuallyEq (hfg : f =ᶠ[𝓝 x] g) :
-    IsSubmersionAtOfComplement F I J n f x ↔ IsSubmersionAtOfComplement F I J n g x := by
-  simpa only [IsSubmersionAtOfComplement_def] using
-    LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq
-      isLocalSourceTargetProperty_submmersionAtProp hfg
+    IsSubmersionAtOfComplement F I J n f x ↔ IsSubmersionAtOfComplement F I J n g x :=
+  LiftSourceTargetPropertyAt.congr_iff_of_eventuallyEq
+    isLocalSourceTargetProperty_submmersionAtProp hfg
 
 lemma small (hf : IsSubmersionAtOfComplement F I J n f x) : Small.{u} F :=
   small_of_injective <| hf.equiv.symm.injective.comp (Prod.mk_right_injective 0)
@@ -325,7 +312,6 @@ def smallEquiv (hf : IsSubmersionAtOfComplement F I J n f x) : F ≃L[𝕜] hf.s
 
 lemma trans_F (h : IsSubmersionAtOfComplement F I J n f x) (e : F ≃L[𝕜] F') :
     IsSubmersionAtOfComplement F' I J n f x := by
-  rw [IsSubmersionAtOfComplement_def]
   refine ⟨h.domChart, h.codChart, h.mem_domChart_source, h.mem_codChart_source,
     h.domChart_mem_maximalAtlas, h.codChart_mem_maximalAtlas, h.source_subset_preimage_source, ?_⟩
   use h.equiv.trans ((ContinuousLinearEquiv.refl 𝕜 E'').prodCongr e)
@@ -341,7 +327,6 @@ lemma congr_F (e : F ≃L[𝕜] F') :
 /- The set of points where `IsSubmersionAtOfComplement` holds is open. -/
 lemma _root_.isOpen_isSubmersionAt :
     IsOpen {x | IsSubmersionAtOfComplement F I J n f x} := by
-  simp_rw [IsSubmersionAtOfComplement_def]
   exact IsOpen.liftSourceTargetPropertyAt
 
 set_option backward.isDefEq.respectTransparency false in
@@ -352,7 +337,6 @@ theorem prodMap {f : M → N} {g : M' → N'} {x' : M'}
     (hf : IsSubmersionAtOfComplement F I J n f x)
     (hg : IsSubmersionAtOfComplement F' I' J' n g x') :
     IsSubmersionAtOfComplement (F × F') (I.prod I') (J.prod J') n (Prod.map f g) (x, x') := by
-  rw [IsSubmersionAtOfComplement_def]
   apply LiftSourceTargetPropertyAt.prodMap hf.property hg.property
   rintro f φ₁ ψ₁ g φ₂ ψ₂ ⟨equiv₁, hfprop⟩ ⟨equiv₂, hgprop⟩
   use (equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')
@@ -629,8 +613,9 @@ lemma isSubmersionOfComplement_complement (h : IsSubmersion I J n f) :
 /-- If `f` is a submersion, it is an submersion at each point.
 -/
 lemma isSubmersionAt (h : IsSubmersion I J n f) (x : M) : IsSubmersionAt I J n f x := by
-  rw [IsSubmersionAt_def]
-  use h.complement, by infer_instance, by infer_instance, h.isSubmersionOfComplement_complement x
+  rw [IsSubmersionAt]
+  use h.complement, by infer_instance, by infer_instance
+  exact h.isSubmersionOfComplement_complement x
 
 /-- If `f = g` and `f` is a submersion, so is `g`. -/
 theorem congr (h : IsSubmersion I J n f) (heq : f = g) : IsSubmersion I J n g :=
@@ -646,8 +631,9 @@ theorem prodMap {f : M → N} {g : M' → N'}
     hg.isSubmersionOfComplement_complement ).isSubmersion
 
 /-- The identity map is an submersion. -/
-protected lemma id [IsManifold I n M] : IsSubmersion I I n (@id M) :=
-  ⟨PUnit, by infer_instance, by infer_instance, IsSubmersionOfComplement.id⟩
+protected lemma id [IsManifold I n M] : IsSubmersion I I n (@id M) := by
+  use PUnit, by infer_instance, by infer_instance
+  exact IsSubmersionOfComplement.id
 
 end IsSubmersion
 

From f7ce3f1b26377c08b9770f39051122d77a1d802d Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Wed, 6 May 2026 15:23:49 +0200
Subject: [PATCH 17/18] wip: no_expose'ing IsSubmersion creates issues with the
 instance below

---
 Mathlib/Geometry/Manifold/Submersion.lean | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index ff03d7b09bdf07..6016912c14c726 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -166,7 +166,7 @@ a submersion at `x` includes a choice of linear isomorphism between `E` and `E''
 where the choice of `F` enters.
 If you need stronger control over the complement `F`, use `IsSubmersionAtOfComplement` instead.
 -/
-irreducible_def IsSubmersionAt (f : M → N) (x : M) : Prop :=
+@[no_expose] def IsSubmersionAt (f : M → N) (x : M) : Prop :=
   ∃ (F : Type u) (_ : NormedAddCommGroup F) (_ : NormedSpace 𝕜 F),
     IsSubmersionAtOfComplement F I J n f x
 
@@ -350,7 +350,6 @@ while being a submersion at `x` requires the existence of a complement in the sa
 the model normed space of `N`. This is solved by `smallComplement` and `smallEquiv`. -/
 lemma isSubmersionAt (h : IsSubmersionAtOfComplement F I J n f x) :
     IsSubmersionAt I J n f x := by
-  rw [IsSubmersionAt_def]
   use h.smallComplement, by infer_instance, by infer_instance
   exact (IsSubmersionAtOfComplement.congr_F h.smallEquiv).mp h
 
@@ -366,7 +365,6 @@ lemma mk_of_charts (equiv : E ≃L[𝕜] (E'' × F))
     (hsource : domChart.source ⊆ f ⁻¹' codChart.source)
     (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
       (domChart.extend I).target) : IsSubmersionAt I J n f x := by
-  rw [IsSubmersionAt_def]
   have aux : IsSubmersionAtOfComplement F I J n f x := by
     apply IsSubmersionAtOfComplement.mk_of_charts <;> assumption
   use aux.smallComplement, by infer_instance, by infer_instance
@@ -383,7 +381,6 @@ lemma mk_of_continuousAt {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv :
     (hcodChart : codChart ∈ IsManifold.maximalAtlas J n N)
     (hwrittenInExtend : EqOn ((codChart.extend J) ∘ f ∘ (domChart.extend I).symm) (Prod.fst ∘ equiv)
       (domChart.extend I).target) : IsSubmersionAt I J n f x := by
-  rw [IsSubmersionAt_def]
   have aux : IsSubmersionAtOfComplement F I J n f x := by
     apply IsSubmersionAtOfComplement.mk_of_continuousAt <;> assumption
   use aux.smallComplement, by infer_instance, by infer_instance
@@ -391,12 +388,10 @@ lemma mk_of_continuousAt {f : M → N} {x : M} (hf : ContinuousAt f x) (equiv :
 
 /-- A choice of complement of the model normed space `E` of `M` in the model normed space
 `E'` of `N` -/
-def complement (h : IsSubmersionAt I J n f x) : Type u := by
-  rw [IsSubmersionAt_def] at h
-  exact Classical.choose h
+@[no_expose] def complement (h : IsSubmersionAt I J n f x) : Type u := Classical.choose h
 
 instance (h : IsSubmersionAt I J n f x) : NormedAddCommGroup h.complement := by
-  rw [IsSubmersionAt_def] at h
+  unfold IsSubmersionAt at h--rw [IsSubmersionAt_def] at h
   exact Classical.choose <| Classical.choose_spec h
 
 instance (h : IsSubmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by
@@ -474,7 +469,6 @@ lemma target_subset_preimage_target (h : IsSubmersionAt I J n f x) :
 then `g` is a submersion at `x`. -/
 lemma congr_of_eventuallyEq (hf : IsSubmersionAt I J n f x) (hfg : f =ᶠ[𝓝 x] g) :
     IsSubmersionAt I J n g x := by
-  rw [IsSubmersionAt_def]
   use hf.complement, by infer_instance, by infer_instance
   exact hf.isSubmersionAtOfComplement_complement.congr_of_eventuallyEq hfg
 

From 5417e2daa6aabd13d1a8e8e58df6dc5cad97f8ea Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Thu, 7 May 2026 11:41:52 +0200
Subject: [PATCH 18/18] chore: add schmeding reference

---
 Mathlib/Geometry/Manifold/Submersion.lean |  5 +++++
 docs/references.bib                       | 15 +++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/Mathlib/Geometry/Manifold/Submersion.lean b/Mathlib/Geometry/Manifold/Submersion.lean
index 6016912c14c726..f02eeb24e82748 100644
--- a/Mathlib/Geometry/Manifold/Submersion.lean
+++ b/Mathlib/Geometry/Manifold/Submersion.lean
@@ -81,6 +81,11 @@ if there exist charts near `x` and `f x` in which `f` looks like the standard pr
   a local diffeomorphism (at `x`) is a submersion (at `x`)
 * `Diffeomorph.isSubmersion`: in particular, a diffeomorphism is a submersion
 
+## References
+
+* [Alexander Schmeding, *An introduction to infinite-dimensional differential geometry*][schmeding2023]
+* Note that Margelef-Roig and Dominguez have a slightly different definition of submersions.
+
 **Please do not work** on this file without prior discussion with Michael Rothgang.
 This will be the topic of Samantha Naranjo's master's thesis, and it's nice to coordinate.
 
diff --git a/docs/references.bib b/docs/references.bib
index ab1142d7dfe900..7ce6c9bd1934b0 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -5037,6 +5037,21 @@ @Misc{            schleicher_stoll
   url           = {http://www.cs.cmu.edu/afs/cs/academic/class/15859-s05/www/lecture-notes/comb-games-notes.pdf}
 }
 
+@Book{            schmeding2023,
+  author        = {Schmeding, Alexander},
+  title         = {An introduction to infinite-dimensional differential
+                  geometry},
+  series        = {Cambridge Studies in Advanced Mathematics},
+  volume        = {202},
+  publisher     = {Cambridge University Press, Cambridge},
+  year          = {2023},
+  pages         = {xiv+267},
+  isbn          = {978-1-316-51488-7},
+  mrclass       = {58-02 (22E65 46-02 53-02 58B25 58D05 58D15 58H05)},
+  mrnumber      = {4505843},
+  mrreviewer    = {Thomas\ O.\ Rot}
+}
+
 @Misc{            scholze2011perfectoid,
   title         = {Perfectoid spaces},
   author        = {Peter Scholze},