chore: rename LocalEquiv to PartialEquiv (#8984)

The current name is misleading: there's no open set involved; it's just an equivalence between subsets of domain and target.
[zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20around.20local.20homeomorphisms/near/407090631)

`PEquiv` is similarly named: this is fine, as they're different designs for the same concept.



Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>

Mathlib.lean

@@ -2496,9 +2496,9 @@ import Mathlib.Logic.Equiv.Fin
 import Mathlib.Logic.Equiv.Fintype
 import Mathlib.Logic.Equiv.Functor
 import Mathlib.Logic.Equiv.List
-import Mathlib.Logic.Equiv.LocalEquiv
 import Mathlib.Logic.Equiv.Nat
 import Mathlib.Logic.Equiv.Option
+import Mathlib.Logic.Equiv.PartialEquiv
 import Mathlib.Logic.Equiv.Set
 import Mathlib.Logic.Equiv.TransferInstance
 import Mathlib.Logic.Function.Basic

Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

@@ -18,9 +18,12 @@ When `f'` is onto, we show that `f` is locally onto.
 When `f'` is a continuous linear equiv, we show that `f` is a homeomorphism
 between `s` and `f '' s`. More precisely, we define `ApproximatesLinearOn.toPartialHomeomorph` to
 be a `PartialHomeomorph` with `toFun = f`, `source = s`, and `target = f '' s`.
+between `s` and `f '' s`. More precisely, we define `ApproximatesLinearOn.toPartialHomeomorph` to
+be a `PartialHomeomorph` with `toFun = f`, `source = s`, and `target = f '' s`.
 
 Maps of this type naturally appear in the proof of the inverse function theorem (see next section),
 and `ApproximatesLinearOn.toPartialHomeomorph` will imply that the locally inverse function
+and `ApproximatesLinearOn.toPartialHomeomorph` will imply that the locally inverse function
 exists.
 
 We define this auxiliary notion to split the proof of the inverse function theorem into small
@@ -356,25 +359,25 @@ protected theorem surjective [CompleteSpace E] (hf : ApproximatesLinearOn f (f'
 Should not be used outside of this file, because it is superseded by `toPartialHomeomorph` below.
 
 This is a first step towards the inverse function. -/
-def toLocalEquiv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
-    (hc : Subsingleton E ∨ c < N⁻¹) : LocalEquiv E F :=
-  (hf.injOn hc).toLocalEquiv _ _
-#align approximates_linear_on.to_local_equiv ApproximatesLinearOn.toLocalEquiv
+def toPartialEquiv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
+    (hc : Subsingleton E ∨ c < N⁻¹) : PartialEquiv E F :=
+  (hf.injOn hc).toPartialEquiv _ _
+#align approximates_linear_on.to_local_equiv ApproximatesLinearOn.toPartialEquiv
 
 /-- The inverse function is continuous on `f '' s`.
 Use properties of `PartialHomeomorph` instead. -/
 theorem inverse_continuousOn (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
-    (hc : Subsingleton E ∨ c < N⁻¹) : ContinuousOn (hf.toLocalEquiv hc).symm (f '' s) := by
+    (hc : Subsingleton E ∨ c < N⁻¹) : ContinuousOn (hf.toPartialEquiv hc).symm (f '' s) := by
   apply continuousOn_iff_continuous_restrict.2
-  refine' ((hf.antilipschitz hc).to_rightInvOn' _ (hf.toLocalEquiv hc).right_inv').continuous
-  exact fun x hx => (hf.toLocalEquiv hc).map_target hx
+  refine' ((hf.antilipschitz hc).to_rightInvOn' _ (hf.toPartialEquiv hc).right_inv').continuous
+  exact fun x hx => (hf.toPartialEquiv hc).map_target hx
 #align approximates_linear_on.inverse_continuous_on ApproximatesLinearOn.inverse_continuousOn
 
 /-- The inverse function is approximated linearly on `f '' s` by `f'.symm`. -/
 theorem to_inv (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c) (hc : Subsingleton E ∨ c < N⁻¹) :
-    ApproximatesLinearOn (hf.toLocalEquiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s)
+    ApproximatesLinearOn (hf.toPartialEquiv hc).symm (f'.symm : F →L[𝕜] E) (f '' s)
       (N * (N⁻¹ - c)⁻¹ * c) := fun x hx y hy ↦ by
-  set A := hf.toLocalEquiv hc
+  set A := hf.toPartialEquiv hc
   have Af : ∀ z, A z = f z := fun z => rfl
   rcases (mem_image _ _ _).1 hx with ⟨x', x's, rfl⟩
   rcases (mem_image _ _ _).1 hy with ⟨y', y's, rfl⟩
@@ -403,7 +406,7 @@ variable (f s)
 returns a local homeomorph with `toFun = f` and `source = s`. -/
 def toPartialHomeomorph (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
     (hc : Subsingleton E ∨ c < N⁻¹) (hs : IsOpen s) : PartialHomeomorph E F where
-  toLocalEquiv := hf.toLocalEquiv hc
+  toPartialEquiv := hf.toPartialEquiv hc
   open_source := hs
   open_target := hf.open_image f'.toNonlinearRightInverse hs <| by
     rwa [f'.toEquiv.subsingleton_congr] at hc

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -12,8 +12,8 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Log
 # Maps on the unit circle
 
 In this file we prove some basic lemmas about `expMapCircle` and the restriction of `Complex.arg`
-to the unit circle. These two maps define a local equivalence between `circle` and `ℝ`, see
-`circle.argLocalEquiv` and `circle.argEquiv`, that sends the whole circle to `(-π, π]`.
+to the unit circle. These two maps define a partial equivalence between `circle` and `ℝ`, see
+`circle.argPartialEquiv` and `circle.argEquiv`, that sends the whole circle to `(-π, π]`.
 -/
 
 
@@ -45,10 +45,10 @@ theorem expMapCircle_arg (z : circle) : expMapCircle (arg z) = z :=
 
 namespace circle
 
-/-- `Complex.arg ∘ (↑)` and `expMapCircle` define a local equivalence between `circle` and `ℝ`
+/-- `Complex.arg ∘ (↑)` and `expMapCircle` define a partial equivalence between `circle` and `ℝ`
 with `source = Set.univ` and `target = Set.Ioc (-π) π`. -/
 @[simps (config := .asFn)]
-noncomputable def argLocalEquiv : LocalEquiv circle ℝ where
+noncomputable def argPartialEquiv : PartialEquiv circle ℝ where
   toFun := arg ∘ (↑)
   invFun := expMapCircle
   source := univ
@@ -57,15 +57,15 @@ noncomputable def argLocalEquiv : LocalEquiv circle ℝ where
   map_target' := mapsTo_univ _ _
   left_inv' z _ := expMapCircle_arg z
   right_inv' _ hx := arg_expMapCircle hx.1 hx.2
-#align circle.arg_local_equiv circle.argLocalEquiv
+#align circle.arg_local_equiv circle.argPartialEquiv
 
 /-- `Complex.arg` and `expMapCircle` define an equivalence between `circle` and `(-π, π]`. -/
 @[simps (config := .asFn)]
 noncomputable def argEquiv : circle ≃ Ioc (-π) π where
   toFun z := ⟨arg z, neg_pi_lt_arg _, arg_le_pi _⟩
   invFun := expMapCircle ∘ (↑)
-  left_inv _ := argLocalEquiv.left_inv trivial
-  right_inv x := Subtype.ext <| argLocalEquiv.right_inv x.2
+  left_inv _ := argPartialEquiv.left_inv trivial
+  right_inv x := Subtype.ext <| argPartialEquiv.right_inv x.2
 #align circle.arg_equiv circle.argEquiv
 
 end circle
@@ -75,11 +75,11 @@ theorem leftInverse_expMapCircle_arg : LeftInverse expMapCircle (arg ∘ (↑))
 #align left_inverse_exp_map_circle_arg leftInverse_expMapCircle_arg
 
 theorem invOn_arg_expMapCircle : InvOn (arg ∘ (↑)) expMapCircle (Ioc (-π) π) univ :=
-  circle.argLocalEquiv.symm.invOn
+  circle.argPartialEquiv.symm.invOn
 #align inv_on_arg_exp_map_circle invOn_arg_expMapCircle
 
 theorem surjOn_expMapCircle_neg_pi_pi : SurjOn expMapCircle (Ioc (-π) π) univ :=
-  circle.argLocalEquiv.symm.surjOn
+  circle.argPartialEquiv.symm.surjOn
 #align surj_on_exp_map_circle_neg_pi_pi surjOn_expMapCircle_neg_pi_pi
 
 theorem expMapCircle_eq_expMapCircle {x y : ℝ} :

Mathlib/Data/PEquiv.lean

@@ -43,7 +43,7 @@ pequiv, partial equivalence
 universe u v w x
 
 /-- A `PEquiv` is a partial equivalence, a representation of a bijection between a subset
-  of `α` and a subset of `β`. See also `LocalEquiv` for a version that requires `toFun` and
+  of `α` and a subset of `β`. See also `PartialEquiv` for a version that requires `toFun` and
 `invFun` to be globally defined functions and has `source` and `target` sets as extra fields. -/
 structure PEquiv (α : Type u) (β : Type v) where
   /-- The underlying partial function of a `PEquiv` -/
@@ -55,7 +55,7 @@ structure PEquiv (α : Type u) (β : Type v) where
 #align pequiv PEquiv
 
 /-- A `PEquiv` is a partial equivalence, a representation of a bijection between a subset
-  of `α` and a subset of `β`. See also `LocalEquiv` for a version that requires `toFun` and
+  of `α` and a subset of `β`. See also `PartialEquiv` for a version that requires `toFun` and
 `invFun` to be globally defined functions and has `source` and `target` sets as extra fields. -/
 infixr:25 " ≃. " => PEquiv
 

Mathlib/Geometry/Manifold/ChartedSpace.lean

@@ -122,12 +122,12 @@ universe u
 variable {H : Type u} {H' : Type*} {M : Type*} {M' : Type*} {M'' : Type*}
 
 /- Notational shortcut for the composition of local homeomorphisms and local equivs, i.e.,
-`PartialHomeomorph.trans` and `LocalEquiv.trans`.
+`PartialHomeomorph.trans` and `PartialEquiv.trans`.
 Note that, as is usual for equivs, the composition is from left to right, hence the direction of
 the arrow. -/
 scoped[Manifold] infixr:100 " ≫ₕ " => PartialHomeomorph.trans
 
-scoped[Manifold] infixr:100 " ≫ " => LocalEquiv.trans
+scoped[Manifold] infixr:100 " ≫ " => PartialEquiv.trans
 
 open Set PartialHomeomorph Manifold  -- Porting note: Added `Manifold`
 
@@ -284,7 +284,7 @@ def idGroupoid (H : Type u) [TopologicalSpace H] : StructureGroupoid H where
     cases' (mem_union _ _ _).1 he with E E
     · simp [mem_singleton_iff.mp E]
     · right
-      simpa only [e.toLocalEquiv.image_source_eq_target.symm, mfld_simps] using E
+      simpa only [e.toPartialEquiv.image_source_eq_target.symm, mfld_simps] using E
   id_mem' := mem_union_left _ rfl
   locality' e he := by
     cases' e.source.eq_empty_or_nonempty with h h
@@ -302,7 +302,7 @@ def idGroupoid (H : Type u) [TopologicalSpace H] : StructureGroupoid H where
         have : (e.restr s).source = univ := by
           rw [hs]
           simp
-        have : e.toLocalEquiv.source ∩ interior s = univ := this
+        have : e.toPartialEquiv.source ∩ interior s = univ := this
         have : univ ⊆ interior s := by
           rw [← this]
           exact inter_subset_right _ _
@@ -319,7 +319,7 @@ def idGroupoid (H : Type u) [TopologicalSpace H] : StructureGroupoid H where
           rw [Set.mem_singleton_iff.1 he] <;> rfl
       rwa [← this]
     · right
-      have he : e.toLocalEquiv.source = ∅ := he
+      have he : e.toPartialEquiv.source = ∅ := he
       rwa [Set.mem_setOf_eq, EqOnSource.source_eq he'e]
 #align id_groupoid idGroupoid
 
@@ -392,7 +392,7 @@ def Pregroupoid.groupoid (PG : Pregroupoid H) : StructureGroupoid H where
       -- convert he.2
       -- rw [A.1]
       -- rfl
-      rw [A.1, symm_toLocalEquiv, LocalEquiv.symm_source]
+      rw [A.1, symm_toPartialEquiv, PartialEquiv.symm_source]
       exact he.2
 #align pregroupoid.groupoid Pregroupoid.groupoid
 
@@ -844,23 +844,23 @@ charts that are only local equivs, and continuity properties for their compositi
 This is formalised in `ChartedSpaceCore`. -/
 -- @[nolint has_nonempty_instance]  -- Porting note: commented out
 structure ChartedSpaceCore (H : Type*) [TopologicalSpace H] (M : Type*) where
-  atlas : Set (LocalEquiv M H)
-  chartAt : M → LocalEquiv M H
+  atlas : Set (PartialEquiv M H)
+  chartAt : M → PartialEquiv M H
   mem_chart_source : ∀ x, x ∈ (chartAt x).source
   chart_mem_atlas : ∀ x, chartAt x ∈ atlas
-  open_source : ∀ e e' : LocalEquiv M H, e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source
-  continuousOn_toFun : ∀ e e' : LocalEquiv M H, e ∈ atlas → e' ∈ atlas →
+  open_source : ∀ e e' : PartialEquiv M H, e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source
+  continuousOn_toFun : ∀ e e' : PartialEquiv M H, e ∈ atlas → e' ∈ atlas →
     ContinuousOn (e.symm.trans e') (e.symm.trans e').source
 #align charted_space_core ChartedSpaceCore
 
 namespace ChartedSpaceCore
 
-variable [TopologicalSpace H] (c : ChartedSpaceCore H M) {e : LocalEquiv M H}
+variable [TopologicalSpace H] (c : ChartedSpaceCore H M) {e : PartialEquiv M H}
 
 /-- Topology generated by a set of charts on a Type. -/
 protected def toTopologicalSpace : TopologicalSpace M :=
   TopologicalSpace.generateFrom <|
-    ⋃ (e : LocalEquiv M H) (_ : e ∈ c.atlas) (s : Set H) (_ : IsOpen s),
+    ⋃ (e : PartialEquiv M H) (_ : e ∈ c.atlas) (s : Set H) (_ : IsOpen s),
       {e ⁻¹' s ∩ e.source}
 #align charted_space_core.to_topological_space ChartedSpaceCore.toTopologicalSpace
 
@@ -874,14 +874,14 @@ theorem open_source' (he : e ∈ c.atlas) : IsOpen[c.toTopologicalSpace] e.sourc
 theorem open_target (he : e ∈ c.atlas) : IsOpen e.target := by
   have E : e.target ∩ e.symm ⁻¹' e.source = e.target :=
     Subset.antisymm (inter_subset_left _ _) fun x hx ↦
-      ⟨hx, LocalEquiv.target_subset_preimage_source _ hx⟩
-  simpa [LocalEquiv.trans_source, E] using c.open_source e e he he
+      ⟨hx, PartialEquiv.target_subset_preimage_source _ hx⟩
+  simpa [PartialEquiv.trans_source, E] using c.open_source e e he he
 #align charted_space_core.open_target ChartedSpaceCore.open_target
 
 /-- An element of the atlas in a charted space without topology becomes a local homeomorphism
 for the topology constructed from this atlas. The `localHomeomorph` version is given in this
 definition. -/
-protected def localHomeomorph (e : LocalEquiv M H) (he : e ∈ c.atlas) :
+protected def localHomeomorph (e : PartialEquiv M H) (he : e ∈ c.atlas) :
     @PartialHomeomorph M H c.toTopologicalSpace _ :=
   { c.toTopologicalSpace, e with
     open_source := by convert c.open_source' he
@@ -910,14 +910,14 @@ protected def localHomeomorph (e : LocalEquiv M H) (he : e ∈ c.atlas) :
         rw [← inter_assoc, ← inter_assoc]
         congr 1
         exact inter_comm _ _
-      simpa [LocalEquiv.trans_source, preimage_inter, preimage_comp.symm, A] using this }
+      simpa [PartialEquiv.trans_source, preimage_inter, preimage_comp.symm, A] using this }
 #align charted_space_core.local_homeomorph ChartedSpaceCore.localHomeomorph
 
 /-- Given a charted space without topology, endow it with a genuine charted space structure with
 respect to the topology constructed from the atlas. -/
 def toChartedSpace : @ChartedSpace H _ M c.toTopologicalSpace :=
   { c.toTopologicalSpace with
-    atlas := ⋃ (e : LocalEquiv M H) (he : e ∈ c.atlas), {c.localHomeomorph e he}
+    atlas := ⋃ (e : PartialEquiv M H) (he : e ∈ c.atlas), {c.localHomeomorph e he}
     chartAt := fun x ↦ c.localHomeomorph (c.chartAt x) (c.chart_mem_atlas x)
     mem_chart_source := fun x ↦ c.mem_chart_source x
     chart_mem_atlas := fun x ↦ by

Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

@@ -106,7 +106,7 @@ theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I M) :
     ContMDiffOn 𝓘(𝕜, E) I n (e.extend I).symm (I '' e.target) := by
   refine (contMDiffOn_symm_of_mem_maximalAtlas he).comp
     (contMDiffOn_model_symm.mono <| image_subset_range _ _) ?_
-  simp_rw [image_subset_iff, LocalEquiv.restr_coe_symm, I.toLocalEquiv_coe_symm,
+  simp_rw [image_subset_iff, PartialEquiv.restr_coe_symm, I.toPartialEquiv_coe_symm,
     preimage_preimage, I.left_inv, preimage_id']; rfl
 #align cont_mdiff_on_extend_symm contMDiffOn_extend_symm
 

Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

@@ -359,8 +359,8 @@ theorem contMDiffWithinAt_iff_target :
     ContinuousWithinAt f s x ∧ ContinuousWithinAt (extChartAt I' (f x) ∘ f) s x ↔
         ContinuousWithinAt f s x :=
       and_iff_left_of_imp <| (continuousAt_extChartAt _ _).comp_continuousWithinAt
-  simp_rw [cont, ContDiffWithinAtProp, extChartAt, PartialHomeomorph.extend, LocalEquiv.coe_trans,
-    ModelWithCorners.toLocalEquiv_coe, PartialHomeomorph.coe_coe, modelWithCornersSelf_coe,
+  simp_rw [cont, ContDiffWithinAtProp, extChartAt, PartialHomeomorph.extend, PartialEquiv.coe_trans,
+    ModelWithCorners.toPartialEquiv_coe, PartialHomeomorph.coe_coe, modelWithCornersSelf_coe,
     chartAt_self_eq, PartialHomeomorph.refl_apply, comp.left_id]
   rfl
 #align cont_mdiff_within_at_iff_target contMDiffWithinAt_iff_target
@@ -582,8 +582,8 @@ theorem contMDiffOn_iff_target :
         ∀ y : M',
           ContMDiffOn I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source) := by
   simp only [contMDiffOn_iff, ModelWithCorners.source_eq, chartAt_self_eq,
-    PartialHomeomorph.refl_localEquiv, LocalEquiv.refl_trans, extChartAt, PartialHomeomorph.extend,
-    Set.preimage_univ, Set.inter_univ, and_congr_right_iff]
+    PartialHomeomorph.refl_localEquiv, PartialEquiv.refl_trans, extChartAt,
+    PartialHomeomorph.extend, Set.preimage_univ, Set.inter_univ, and_congr_right_iff]
   intro h
   constructor
   · refine' fun h' y => ⟨_, fun x _ => h' x y⟩
@@ -838,7 +838,7 @@ theorem contMDiffWithinAt_iff_contMDiffOn_nhds {n : ℕ} :
     have hv₂ : MapsTo f ((extChartAt I x).symm '' v) (extChartAt I' (f x)).source := by
       rintro _ ⟨y, hy, rfl⟩
       exact (hsub hy).2.2
-    rwa [contMDiffOn_iff_of_subset_source' hv₁ hv₂, LocalEquiv.image_symm_image_of_subset_target]
+    rwa [contMDiffOn_iff_of_subset_source' hv₁ hv₂, PartialEquiv.image_symm_image_of_subset_target]
     exact hsub.trans (inter_subset_left _ _)
 #align cont_mdiff_within_at_iff_cont_mdiff_on_nhds contMDiffWithinAt_iff_contMDiffOn_nhds
 

Mathlib/Geometry/Manifold/ContMDiff/Product.lean

@@ -405,7 +405,7 @@ theorem contMDiffWithinAt_pi_space :
   -- Porting note: `simp` fails to apply it on the LHS
   rw [contMDiffWithinAt_iff]
   simp only [contMDiffWithinAt_iff, continuousWithinAt_pi, contDiffWithinAt_pi, forall_and,
-    writtenInExtChartAt, extChartAt_model_space_eq_id, (· ∘ ·), LocalEquiv.refl_coe, id]
+    writtenInExtChartAt, extChartAt_model_space_eq_id, (· ∘ ·), PartialEquiv.refl_coe, id]
 #align cont_mdiff_within_at_pi_space contMDiffWithinAt_pi_space
 
 theorem contMDiffOn_pi_space :

Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

@@ -97,7 +97,7 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N →
           (range I) (extChartAt I (g x₀) (g ((extChartAt J x₀).symm x))))
       (range J) (extChartAt J x₀ x₀) := by
     rw [contMDiffAt_iff] at hf hg
-    simp_rw [Function.comp, uncurry, extChartAt_prod, LocalEquiv.prod_coe_symm,
+    simp_rw [Function.comp, uncurry, extChartAt_prod, PartialEquiv.prod_coe_symm,
       ModelWithCorners.range_prod] at hf ⊢
     refine' ContDiffWithinAt.fderivWithin _ hg.2 I.unique_diff hmn (mem_range_self _) _
     · simp_rw [extChartAt_to_inv]; exact hf.2
@@ -161,11 +161,11 @@ protected theorem ContMDiffAt.mfderiv {x₀ : N} (f : N → M → M') (g : N →
     symm
     rw [(h2x₂.mdifferentiableAt le_rfl).mfderiv]
     have hI := (contDiffWithinAt_ext_coord_change I (g x₂) (g x₀) <|
-      LocalEquiv.mem_symm_trans_source _ hx₂ <|
+      PartialEquiv.mem_symm_trans_source _ hx₂ <|
         mem_extChartAt_source I (g x₂)).differentiableWithinAt le_top
     have hI' :=
       (contDiffWithinAt_ext_coord_change I' (f x₀ (g x₀)) (f x₂ (g x₂)) <|
-            LocalEquiv.mem_symm_trans_source _ (mem_extChartAt_source I' (f x₂ (g x₂)))
+            PartialEquiv.mem_symm_trans_source _ (mem_extChartAt_source I' (f x₂ (g x₂)))
               h3x₂).differentiableWithinAt le_top
     have h3f := (h2x₂.mdifferentiableAt le_rfl).2
     refine' fderivWithin.comp₃ _ hI' h3f hI _ _ _ _ (I.unique_diff _ <| mem_range_self _)

Mathlib/Geometry/Manifold/Diffeomorph.lean

@@ -509,7 +509,7 @@ variable (I) (e : E ≃ₘ[𝕜] E')
 
 /-- Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space. -/
 def transDiffeomorph (I : ModelWithCorners 𝕜 E H) (e : E ≃ₘ[𝕜] E') : ModelWithCorners 𝕜 E' H where
-  toLocalEquiv := I.toLocalEquiv.trans e.toEquiv.toLocalEquiv
+  toPartialEquiv := I.toPartialEquiv.trans e.toEquiv.toPartialEquiv
   source_eq := by simp
   unique_diff' := by simp [range_comp e, I.unique_diff]
   continuous_toFun := e.continuous.comp I.continuous

Mathlib/Geometry/Manifold/Instances/Sphere.lean

@@ -430,8 +430,8 @@ instance smoothMfldWithCorners {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
         (ℝ ∙ (v : E))ᗮ.subtypeL.contDiff).comp U.symm.contDiff
       convert H₁.comp' (H₂.contDiffOn : ContDiffOn ℝ ⊤ _ Set.univ) using 1
       -- -- squeezed from `ext, simp [sphere_ext_iff, stereographic'_symm_apply, real_inner_comm]`
-      simp only [PartialHomeomorph.trans_toLocalEquiv, PartialHomeomorph.symm_toLocalEquiv,
-        LocalEquiv.trans_source, LocalEquiv.symm_source, stereographic'_target,
+      simp only [PartialHomeomorph.trans_toPartialEquiv, PartialHomeomorph.symm_toPartialEquiv,
+        PartialEquiv.trans_source, PartialEquiv.symm_source, stereographic'_target,
         stereographic'_source]
       simp only [modelWithCornersSelf_coe, modelWithCornersSelf_coe_symm, Set.preimage_id,
         Set.range_id, Set.inter_univ, Set.univ_inter, Set.compl_singleton_eq, Set.preimage_setOf_eq]