Audit remaining uses; remove almost all of them.

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -1899,7 +1899,7 @@ namespace PartialHomeomorph
 
 variable (𝕜)
 
-/-- Restrict a local homeomorphism to the subsets of the source and target
+/-- Restrict a partial homeomorphism to the subsets of the source and target
 that consist of points `x ∈ f.source`, `y = f x ∈ f.target`
 such that `f` is `C^n` at `x` and `f.symm` is `C^n` at `y`.
 

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

@@ -226,7 +226,7 @@ theorem isLocalStructomorphOn_contDiffGroupoid_iff (f : PartialHomeomorph M M')
       mfld_set_tac
     refine' ⟨e.symm, StructureGroupoid.symm _ he, h3e, _⟩
     rw [h2X]; exact e.mapsTo hex
-  · -- We now show the converse: a local homeomorphism `f : M → M'` which is smooth in both
+  · -- We now show the converse: a partial homeomorphism `f : M → M'` which is smooth in both
     -- directions is a local structomorphism.  We do this by proposing
     -- `((chart_at H x).symm.trans f).trans (chart_at H (f x))` as a candidate for a structomorphism
     -- of `H`.

Mathlib/Geometry/Manifold/LocalInvariantProperties.lean

@@ -636,7 +636,7 @@ theorem isLocalStructomorphWithinAt_localInvariantProp [ClosedUnderRestriction G
       · simpa only [hex, hef ⟨hx, hex⟩, mfld_simps] using hfx }
 #align structure_groupoid.is_local_structomorph_within_at_local_invariant_prop StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp
 
-/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is a local homeomorph.
+/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is a partial homeomorph.
   This gives us an `e` that is defined on a subset of `f.source`. -/
 theorem _root_.PartialHomeomorph.isLocalStructomorphWithinAt_iff {G : StructureGroupoid H}
     [ClosedUnderRestriction G] (f : PartialHomeomorph H H) {s : Set H} {x : H}
@@ -659,7 +659,7 @@ theorem _root_.PartialHomeomorph.isLocalStructomorphWithinAt_iff {G : StructureG
     exact ⟨e, he, hfe, hxe⟩
 #align local_homeomorph.is_local_structomorph_within_at_iff PartialHomeomorph.isLocalStructomorphWithinAt_iff
 
-/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is a local homeomorph and
+/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is a partial homeomorph and
   the set we're considering is a superset of `f.source`. -/
 theorem _root_.PartialHomeomorph.isLocalStructomorphWithinAt_iff' {G : StructureGroupoid H}
     [ClosedUnderRestriction G] (f : PartialHomeomorph H H) {s : Set H} {x : H} (hs : f.source ⊆ s)
@@ -673,7 +673,7 @@ theorem _root_.PartialHomeomorph.isLocalStructomorphWithinAt_iff' {G : Structure
   rw [inter_eq_right.mpr (h2e.trans hs)]
 #align local_homeomorph.is_local_structomorph_within_at_iff' PartialHomeomorph.isLocalStructomorphWithinAt_iff'
 
-/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is a local homeomorph and
+/-- A slight reformulation of `IsLocalStructomorphWithinAt` when `f` is a partial homeomorph and
   the set we're considering is `f.source`. -/
 theorem _root_.PartialHomeomorph.isLocalStructomorphWithinAt_source_iff {G : StructureGroupoid H}
     [ClosedUnderRestriction G] (f : PartialHomeomorph H H) {x : H} :

Mathlib/Geometry/Manifold/MFDeriv.lean

@@ -242,7 +242,7 @@ def MDifferentiable (f : M → M') :=
   ∀ x, MDifferentiableAt I I' f x
 #align mdifferentiable MDifferentiable
 
-/-- Prop registering if a local homeomorphism is a local diffeomorphism on its source -/
+/-- Prop registering if a partial homeomorphism is a local diffeomorphism on its source -/
 def PartialHomeomorph.MDifferentiable (f : PartialHomeomorph M M') :=
   MDifferentiableOn I I' f f.source ∧ MDifferentiableOn I' I f.symm f.target
 #align local_homeomorph.mdifferentiable PartialHomeomorph.MDifferentiable
@@ -1898,7 +1898,7 @@ end Charts
 
 end SpecificFunctions
 
-/-! ### Differentiable local homeomorphisms -/
+/-! ### Differentiable partial homeomorphisms -/
 
 namespace PartialHomeomorph.MDifferentiable
 
@@ -1944,7 +1944,7 @@ theorem comp_symm_deriv {x : M'} (hx : x ∈ e.target) :
   he.symm.symm_comp_deriv hx
 #align local_homeomorph.mdifferentiable.comp_symm_deriv PartialHomeomorph.MDifferentiable.comp_symm_deriv
 
-/-- The derivative of a differentiable local homeomorphism, as a continuous linear equivalence
+/-- The derivative of a differentiable partial homeomorphism, as a continuous linear equivalence
 between the tangent spaces at `x` and `e x`. -/
 protected def mfderiv {x : M} (hx : x ∈ e.source) : TangentSpace I x ≃L[𝕜] TangentSpace I' (e x) :=
   { mfderiv I I' e x with

Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

@@ -37,7 +37,7 @@ but add these assumptions later as needed. (Quite a few results still do not req
 * `modelWithCornersSelf 𝕜 E` :
   trivial model with corners structure on the space `E` embedded in itself by the identity.
 * `contDiffGroupoid n I` :
-  when `I` is a model with corners on `(𝕜, E, H)`, this is the groupoid of local homeos of `H`
+  when `I` is a model with corners on `(𝕜, E, H)`, this is the groupoid of partial homeos of `H`
   which are of class `C^n` over the normed field `𝕜`, when read in `E`.
 * `SmoothManifoldWithCorners I M` :
   a type class saying that the charted space `M`, modelled on the space `H`, has `C^∞` changes of
@@ -46,8 +46,9 @@ but add these assumptions later as needed. (Quite a few results still do not req
 * `extChartAt I x`:
   in a smooth manifold with corners with the model `I` on `(E, H)`, the charts take values in `H`,
   but often we may want to use their `E`-valued version, obtained by composing the charts with `I`.
-  Since the target is in general not open, we can not register them as local homeomorphisms, but
-  we register them as local equivs. `extChartAt I x` is the canonical such local equiv around `x`.
+  Since the target is in general not open, we can not register them as partial homeomorphisms, but
+  we register them as `PartialEquiv`s.
+  `extChartAt I x` is the canonical such partial equiv around `x`.
 
 As specific examples of models with corners, we define (in the file `real_instances.lean`)
 * `modelWithCornersSelf ℝ (EuclideanSpace (Fin n))` for the model space used to define
@@ -177,7 +178,7 @@ switch to this behavior later, doing it mid-port will break a lot of proofs. -/
 
 instance : CoeFun (ModelWithCorners 𝕜 E H) fun _ => H → E := ⟨toFun'⟩
 
-/-- The inverse to a model with corners, only registered as a local equiv. -/
+/-- The inverse to a model with corners, only registered as a `PartialEquiv`. -/
 protected def symm : PartialEquiv E H :=
   I.toPartialEquiv.symm
 #align model_with_corners.symm ModelWithCorners.symm
@@ -374,7 +375,7 @@ section
 
 variable (𝕜 E)
 
-/-- In the trivial model with corners, the associated local equiv is the identity. -/
+/-- In the trivial model with corners, the associated `PartialEquiv` is the identity. -/
 @[simp, mfld_simps]
 theorem modelWithCornersSelf_localEquiv : 𝓘(𝕜, E).toPartialEquiv = PartialEquiv.refl E :=
   rfl
@@ -583,11 +584,11 @@ theorem contDiffGroupoid_le (h : m ≤ n) : contDiffGroupoid n I ≤ contDiffGro
 #align cont_diff_groupoid_le contDiffGroupoid_le
 
 /-- The groupoid of `0`-times continuously differentiable maps is just the groupoid of all
-local homeomorphisms -/
+partial homeomorphisms -/
 theorem contDiffGroupoid_zero_eq : contDiffGroupoid 0 I = continuousGroupoid H := by
   apply le_antisymm le_top
   intro u _
-  -- we have to check that every local homeomorphism belongs to `contDiffGroupoid 0 I`,
+  -- we have to check that every partial homeomorphism belongs to `contDiffGroupoid 0 I`,
   -- by unfolding its definition
   change u ∈ contDiffGroupoid 0 I
   rw [contDiffGroupoid, mem_groupoid_of_pregroupoid]
@@ -601,7 +602,7 @@ theorem contDiffGroupoid_zero_eq : contDiffGroupoid 0 I = continuousGroupoid H :
 
 variable (n)
 
-/-- An identity local homeomorphism belongs to the `C^n` groupoid. -/
+/-- An identity partial homeomorphism belongs to the `C^n` groupoid. -/
 theorem ofSet_mem_contDiffGroupoid {s : Set H} (hs : IsOpen s) :
     PartialHomeomorph.ofSet s hs ∈ contDiffGroupoid n I := by
   rw [contDiffGroupoid, mem_groupoid_of_pregroupoid]
@@ -611,7 +612,7 @@ theorem ofSet_mem_contDiffGroupoid {s : Set H} (hs : IsOpen s) :
   exact this.congr_mono (fun x hx => I.right_inv hx.2) (subset_univ _)
 #align of_set_mem_cont_diff_groupoid ofSet_mem_contDiffGroupoid
 
-/-- The composition of a local homeomorphism from `H` to `M` and its inverse belongs to
+/-- The composition of a partial homeomorphism from `H` to `M` and its inverse belongs to
 the `C^n` groupoid. -/
 theorem symm_trans_mem_contDiffGroupoid (e : PartialHomeomorph M H) :
     e.symm.trans e ∈ contDiffGroupoid n I :=
@@ -622,7 +623,7 @@ theorem symm_trans_mem_contDiffGroupoid (e : PartialHomeomorph M H) :
 
 variable {E' H' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H']
 
-/-- The product of two smooth local homeomorphisms is smooth. -/
+/-- The product of two smooth partial homeomorphisms is smooth. -/
 theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'}
     {e : PartialHomeomorph H H} {e' : PartialHomeomorph H' H'} (he : e ∈ contDiffGroupoid ⊤ I)
     (he' : e' ∈ contDiffGroupoid ⊤ I') : e.prod e' ∈ contDiffGroupoid ⊤ (I.prod I') := by
@@ -744,7 +745,7 @@ def analyticGroupoid : StructureGroupoid H :=
           rw [comp_apply, comp_apply, fg (I.symm y) hy.left.left] at hy
           exact hy.right }
 
-/-- An identity local homeomorphism belongs to the analytic groupoid. -/
+/-- An identity partial homeomorphism belongs to the analytic groupoid. -/
 theorem ofSet_mem_analyticGroupoid {s : Set H} (hs : IsOpen s) :
     PartialHomeomorph.ofSet s hs ∈ analyticGroupoid I := by
   rw [analyticGroupoid]
@@ -770,7 +771,7 @@ theorem ofSet_mem_analyticGroupoid {s : Set H} (hs : IsOpen s) :
     rw [← hy.right, I.right_inv (interior_subset hy.left.right)]
     exact hy.left.right
 
-/-- The composition of a local homeomorphism from `H` to `M` and its inverse belongs to
+/-- The composition of a partial homeomorphism from `H` to `M` and its inverse belongs to
 the analytic groupoid. -/
 theorem symm_trans_mem_analyticGroupoid (e : PartialHomeomorph M H) :
     e.symm.trans e ∈ analyticGroupoid I :=
@@ -788,7 +789,7 @@ instance : ClosedUnderRestriction (analyticGroupoid I) :=
       exact ofSet_mem_analyticGroupoid I hs)
 
 /-- The analytic groupoid on a boundaryless charted space modeled on a complete vector space
-consists of the local homeomorphisms which are analytic and have analytic inverse. -/
+consists of the partial homeomorphisms which are analytic and have analytic inverse. -/
 theorem mem_analyticGroupoid_of_boundaryless [CompleteSpace E] [I.Boundaryless]
     (e : PartialHomeomorph H H) :
     e ∈ analyticGroupoid I ↔ AnalyticOn 𝕜 (I ∘ e ∘ I.symm) (I '' e.source) ∧