diff --git a/Mathlib/Geometry/Manifold/Immersion.lean b/Mathlib/Geometry/Manifold/Immersion.lean
index 412daefb42e3c3..5b95046e925b01 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`.
 
@@ -92,11 +92,9 @@ This shortens the overall argument, as the definition of submersions has the sam
 -/
 
 open scoped Topology ContDiff
-open Function Set Manifold
+open Function Set
 
-@[expose] public section
-
-noncomputable section
+@[expose] public noncomputable section
 
 namespace Manifold
 
@@ -135,11 +133,9 @@ omit [ChartedSpace H M] [ChartedSpace G N] in
 /-- Being an immersion at `x` is a local property. -/
 lemma isLocalSourceTargetProperty_immersionAtProp :
     IsLocalSourceTargetProperty (ImmersionAtProp F I J M N) where
-  mono_source {f φ ψ s} hs hf := by
-    obtain ⟨equiv, hf⟩ := hf
-    exact ⟨equiv, hf.mono (by simp; grind)⟩
-  congr {f g φ ψ} hfg hf := by
-    obtain ⟨equiv, hf⟩ := hf
+  mono_source {f φ ψ s} hs := fun ⟨equiv, hf⟩ ↦ ⟨equiv, hf.mono (by simp; grind)⟩
+  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
@@ -447,11 +443,11 @@ def complement (h : IsImmersionAt I J n f x) : Type u := by
   rw [IsImmersionAt_def] at h
   exact Classical.choose h
 
-noncomputable instance (h : IsImmersionAt I J n f x) : NormedAddCommGroup h.complement := by
+instance (h : IsImmersionAt I J n f x) : NormedAddCommGroup h.complement := by
   rw [IsImmersionAt_def] at h
   exact Classical.choose <| Classical.choose_spec h
 
-noncomputable instance (h : IsImmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by
+instance (h : IsImmersionAt I J n f x) : NormedSpace 𝕜 h.complement := by
   rw [IsImmersionAt_def] at h
   exact Classical.choose <| Classical.choose_spec <| Classical.choose_spec h
 
@@ -684,10 +680,10 @@ variable {f g : M → N}
 `E'` of `N` -/
 def complement (h : IsImmersion I J n f) : Type u := Classical.choose h
 
-noncomputable instance (h : IsImmersion I J n f) : NormedAddCommGroup h.complement :=
+instance (h : IsImmersion I J n f) : NormedAddCommGroup h.complement :=
   Classical.choose <| Classical.choose_spec h
 
-noncomputable instance (h : IsImmersion I J n f) : NormedSpace 𝕜 h.complement :=
+instance (h : IsImmersion I J n f) : NormedSpace 𝕜 h.complement :=
   Classical.choose <| Classical.choose_spec <| Classical.choose_spec h
 
 lemma isImmersionOfComplement_complement (h : IsImmersion I J n f) :