Rename Local to Partial: leanprover-community/mathlib4#8984

Signed-off-by: zeramorphic <[email protected]>

ConNF/FOA/Action/Complete.lean

@@ -53,18 +53,18 @@ theorem disjoint_sandbox :
 This function creates forward and backward images of atoms in the *sandbox litter*,
 a litter which is away from the domain and range of the approximation in question, so it should
 not interfere with other constructions. -/
-noncomputable def atomLocalPerm (hφ : φ.Lawful) : LocalPerm Atom :=
-  LocalPerm.complete φ.atomMapOrElse φ.atomMap.Dom (litterSet φ.sandboxLitter)
+noncomputable def atomPartialPerm (hφ : φ.Lawful) : PartialPerm Atom :=
+  PartialPerm.complete φ.atomMapOrElse φ.atomMap.Dom (litterSet φ.sandboxLitter)
     φ.mk_atomMap_image_le_mk_sandbox
     (by simpa only [mk_litterSet] using Params.κ_isRegular.aleph0_le)
     φ.disjoint_sandbox (φ.atomMapOrElse_injective hφ)
 
 theorem sandboxSubset_small :
     Small
-      (LocalPerm.sandboxSubset φ.mk_atomMap_image_le_mk_sandbox
+      (PartialPerm.sandboxSubset φ.mk_atomMap_image_le_mk_sandbox
         (by simpa only [mk_litterSet] using Params.κ_isRegular.aleph0_le)) := by
   rw [Small]
-  rw [Cardinal.mk_congr (LocalPerm.sandboxSubsetEquiv _ _)]
+  rw [Cardinal.mk_congr (PartialPerm.sandboxSubsetEquiv _ _)]
   simp only [mk_sum, mk_prod, mk_denumerable, lift_aleph0, lift_uzero, lift_id]
   refine' add_lt_of_lt Params.κ_isRegular.aleph0_le _ _ <;>
     refine' mul_lt_of_lt Params.κ_isRegular.aleph0_le
@@ -73,7 +73,7 @@ theorem sandboxSubset_small :
   · exact φ.atomMap_dom_small
   · exact lt_of_le_of_lt mk_image_le φ.atomMap_dom_small
 
-theorem atomLocalPerm_domain_small (hφ : φ.Lawful) : Small (φ.atomLocalPerm hφ).domain :=
+theorem atomPartialPerm_domain_small (hφ : φ.Lawful) : Small (φ.atomPartialPerm hφ).domain :=
   Small.union (Small.union φ.atomMap_dom_small (lt_of_le_of_lt mk_image_le φ.atomMap_dom_small))
     φ.sandboxSubset_small
 
@@ -82,21 +82,21 @@ Its action on atoms matches that of the action, and its rough action on litters
 matches the given litter permutation. -/
 noncomputable def complete (hφ : φ.Lawful) (A : ExtendedIndex β) : NearLitterApprox
     where
-  atomPerm := φ.atomLocalPerm hφ
-  litterPerm := φ.flexibleLitterLocalPerm hφ A
-  domain_small _ := Small.mono (inter_subset_right _ _) (φ.atomLocalPerm_domain_small hφ)
+  atomPerm := φ.atomPartialPerm hφ
+  litterPerm := φ.flexibleLitterPartialPerm hφ A
+  domain_small _ := Small.mono (inter_subset_right _ _) (φ.atomPartialPerm_domain_small hφ)
 
-theorem atomLocalPerm_apply_eq (hφ : φ.Lawful) {a : Atom} (ha : (φ.atomMap a).Dom) :
-    φ.atomLocalPerm hφ a = (φ.atomMap a).get ha := by
-  rwa [atomLocalPerm, LocalPerm.complete_apply_eq, atomMapOrElse_of_dom]
+theorem atomPartialPerm_apply_eq (hφ : φ.Lawful) {a : Atom} (ha : (φ.atomMap a).Dom) :
+    φ.atomPartialPerm hφ a = (φ.atomMap a).get ha := by
+  rwa [atomPartialPerm, PartialPerm.complete_apply_eq, atomMapOrElse_of_dom]
 
 theorem complete_smul_atom_eq {hφ : φ.Lawful} {a : Atom} (ha : (φ.atomMap a).Dom) :
     φ.complete hφ A • a = (φ.atomMap a).get ha :=
-  φ.atomLocalPerm_apply_eq hφ ha
+  φ.atomPartialPerm_apply_eq hφ ha
 
 @[simp]
 theorem complete_smul_litter_eq {hφ : φ.Lawful} (L : Litter) :
-    φ.complete hφ A • L = φ.flexibleLitterLocalPerm hφ A L :=
+    φ.complete hφ A • L = φ.flexibleLitterPartialPerm hφ A L :=
   rfl
 
 theorem smul_atom_eq {hφ : φ.Lawful} {π : NearLitterPerm}
@@ -132,7 +132,7 @@ theorem smul_toNearLitter_eq_of_preciseAt {hφ : φ.Lawful} {π : NearLitterPerm
         exact this
       · exfalso
         refine φ.sandboxLitter_not_banned ?_
-        rw [← eq_of_mem_litterSet_of_mem_litterSet ha (LocalPerm.sandboxSubset_subset _ _ hdom)]
+        rw [← eq_of_mem_litterSet_of_mem_litterSet ha (PartialPerm.sandboxSubset_subset _ _ hdom)]
         exact BannedLitter.litterDom L hL
     · by_contra h'
       simp only [NearLitterPerm.IsException, mem_litterSet, not_or, Classical.not_not, ha] at h
@@ -175,7 +175,7 @@ theorem smul_toNearLitter_eq_of_preciseAt {hφ : φ.Lawful} {π : NearLitterPerm
       rw [this] at h
       exact h hb₁
     · refine' φ.sandboxLitter_not_banned _
-      rw [eq_of_mem_litterSet_of_mem_litterSet (LocalPerm.sandboxSubset_subset _ _ hdom) haL]
+      rw [eq_of_mem_litterSet_of_mem_litterSet (PartialPerm.sandboxSubset_subset _ _ hdom) haL]
       exact BannedLitter.litterMap L hL
 
 theorem smul_nearLitter_eq_of_preciseAt {hφ : φ.Lawful} {π : NearLitterPerm}

ConNF/FOA/Action/FillAtomOrbits.lean

@@ -31,12 +31,12 @@ theorem aleph0_le_not_bannedLitter : ℵ₀ ≤ #{L | ¬φ.BannedLitter L} := by
 
 /-- A local permutation on the set of litters that occur in the domain or range of `w`.
 This permutes both flexible and inflexible litters. -/
-noncomputable def litterPerm' (hφ : φ.Lawful) : LocalPerm Litter :=
-  LocalPerm.complete φ.roughLitterMapOrElse φ.litterMap.Dom {L | ¬φ.BannedLitter L}
+noncomputable def litterPerm' (hφ : φ.Lawful) : PartialPerm Litter :=
+  PartialPerm.complete φ.roughLitterMapOrElse φ.litterMap.Dom {L | ¬φ.BannedLitter L}
     φ.mk_dom_symmDiff_le φ.aleph0_le_not_bannedLitter φ.disjoint_dom_not_bannedLitter
     (φ.roughLitterMapOrElse_injOn hφ)
 
-def idOnBanned (s : Set Litter) : LocalPerm Litter
+def idOnBanned (s : Set Litter) : PartialPerm Litter
     where
   toFun := id
   invFun := id
@@ -46,23 +46,23 @@ def idOnBanned (s : Set Litter) : LocalPerm Litter
   left_inv' _ _ := rfl
   right_inv' _ _ := rfl
 
-noncomputable def litterPerm (hφ : φ.Lawful) : LocalPerm Litter :=
-  LocalPerm.piecewise (φ.litterPerm' hφ) (φ.idOnBanned (φ.litterPerm' hφ).domain)
+noncomputable def litterPerm (hφ : φ.Lawful) : PartialPerm Litter :=
+  PartialPerm.piecewise (φ.litterPerm' hφ) (φ.idOnBanned (φ.litterPerm' hφ).domain)
     (by rw [← Set.subset_compl_iff_disjoint_left]; exact fun L h => h.2)
 
 theorem litterPerm'_apply_eq {φ : NearLitterAction} {hφ : φ.Lawful} (L : Litter)
     (hL : L ∈ φ.litterMap.Dom) : φ.litterPerm' hφ L = φ.roughLitterMapOrElse L :=
-  LocalPerm.complete_apply_eq _ _ _ hL
+  PartialPerm.complete_apply_eq _ _ _ hL
 
 theorem litterPerm_apply_eq {φ : NearLitterAction} {hφ : φ.Lawful} (L : Litter)
     (hL : L ∈ φ.litterMap.Dom) : φ.litterPerm hφ L = φ.roughLitterMapOrElse L := by
   rw [← litterPerm'_apply_eq L hL]
-  exact LocalPerm.piecewise_apply_eq_left (Or.inl (Or.inl hL))
+  exact PartialPerm.piecewise_apply_eq_left (Or.inl (Or.inl hL))
 
 theorem litterPerm'_domain_small (hφ : φ.Lawful) : Small (φ.litterPerm' hφ).domain := by
   refine' Small.union (Small.union φ.litterMap_dom_small φ.litterMap_dom_small.image) _
   rw [Small]
-  rw [Cardinal.mk_congr (LocalPerm.sandboxSubsetEquiv _ _)]
+  rw [Cardinal.mk_congr (PartialPerm.sandboxSubsetEquiv _ _)]
   simp only [mk_sum, mk_prod, mk_denumerable, lift_aleph0, lift_uzero, lift_id]
   refine' add_lt_of_lt Params.κ_isRegular.aleph0_le _ _ <;>
     refine' mul_lt_of_lt Params.κ_isRegular.aleph0_le
@@ -544,7 +544,7 @@ theorem nextImageCore_atom_mem_litter_map (a : Atom) (ha : a ∈ φ.nextImageCor
   obtain ⟨_ | n, a'⟩ | ⟨n, a'⟩ := a' <;>
     simp only [elim_inr, elim_inl, Nat.zero_eq, nextBackwardImage, nextForwardImage] at this ⊢
   · have ha'' := this.2.symm
-    rw [Function.iterate_one, LocalPerm.eq_symm_apply] at ha''
+    rw [Function.iterate_one, PartialPerm.eq_symm_apply] at ha''
     · exact ha''.symm
     · exact hL
     · exact this.1
@@ -593,11 +593,11 @@ theorem nextImageCore_atom_mem
   · intro h
     simp only [mem_symmDiff, SetLike.mem_coe, h, mem_litterSet, true_and, not_true, and_false,
       or_false, not_not] at this
-    rw [ha', ← hL', ← LocalPerm.eq_symm_apply, LocalPerm.left_inv] at this
+    rw [ha', ← hL', ← PartialPerm.eq_symm_apply, PartialPerm.left_inv] at this
     · exact this
     · exact Or.inl (Or.inl (Or.inl hL))
     · exact φ.litter_map_dom_of_mem_nextImageCoreDomain hφ ha
-    · exact LocalPerm.map_domain _ (Or.inl (Or.inl (Or.inl hL)))
+    · exact PartialPerm.map_domain _ (Or.inl (Or.inl (Or.inl hL)))
 
 theorem orbitSetEquiv_atom_mem
     (hdiff : ∀ L hL,
@@ -627,7 +627,7 @@ theorem orbitSetEquiv_atom_mem
     simp only [mem_symmDiff, h, SetLike.mem_coe, mem_litterSet, true_and_iff, not_true,
       and_false_iff, or_false_iff, Classical.not_not] at this
     rw [ha'.1, ← roughLitterMapOrElse_of_dom, ← litterPerm_apply_eq (hφ := hφ), ←
-      LocalPerm.eq_symm_apply, LocalPerm.left_inv] at this
+      PartialPerm.eq_symm_apply, PartialPerm.left_inv] at this
     exact this
     · exact Or.inl (Or.inl (Or.inl hL))
     · exact ha.2
@@ -763,7 +763,7 @@ theorem fillAtomOrbits_precise
         have hbL' := hbL.2
         symm at hbL'
         rw [Function.iterate_succ_apply',
-          LocalPerm.eq_symm_apply _ hL' ((φ.litterPerm hφ).symm.iterate_domain hbL.1)] at hbL'
+          PartialPerm.eq_symm_apply _ hL' ((φ.litterPerm hφ).symm.iterate_domain hbL.1)] at hbL'
         refine' ⟨_, ⟨((φ.litterPerm hφ).symm^[n + 1]) (b : Atom).1, rfl⟩, _, ⟨_, rfl⟩,
           ⟨(φ.orbitSetEquiv (φ.litterPerm hφ (a : Atom).1)).symm (inl (n, b)), _⟩, _⟩
         · exact (φ.litterPerm hφ).symm.iterate_domain hbL.1
@@ -865,7 +865,7 @@ theorem fillAtomOrbits_precise
         rw [← ha'] at this
         simp only [Equiv.apply_symm_apply, elim_inl, nextBackwardImageDomain,
           Function.comp_apply, mem_setOf_eq] at this
-        rw [← this.2, Function.iterate_succ_apply', LocalPerm.right_inv]
+        rw [← this.2, Function.iterate_succ_apply', PartialPerm.right_inv]
         exact (φ.litterPerm hφ).symm.iterate_domain this.1
       · have := φ.orbitSetEquiv_elim_of_mem_nextImageCoreDomain hφ ha₁
         rw [← ha'] at this

ConNF/FOA/Action/NearLitterAction.lean

@@ -286,24 +286,24 @@ theorem roughLitterMapOrElse_injOn_dom_inter_flexible (hφ : φ.Lawful) :
     InjOn φ.roughLitterMapOrElse (φ.litterMap.Dom ∩ {L | Flexible A L}) :=
   (φ.roughLitterMapOrElse_injOn hφ).mono (inter_subset_left _ _)
 
-noncomputable def flexibleLitterLocalPerm (hφ : φ.Lawful) (A : ExtendedIndex β) : LocalPerm Litter :=
-  LocalPerm.complete φ.roughLitterMapOrElse (φ.litterMap.Dom ∩ {L | Flexible A L})
+noncomputable def flexibleLitterPartialPerm (hφ : φ.Lawful) (A : ExtendedIndex β) : PartialPerm Litter :=
+  PartialPerm.complete φ.roughLitterMapOrElse (φ.litterMap.Dom ∩ {L | Flexible A L})
     {L | ¬φ.BannedLitter L ∧ Flexible A L} φ.mk_dom_inter_flexible_symmDiff_le
     φ.aleph0_le_not_bannedLitter_and_flexible φ.disjoint_dom_inter_flexible_not_bannedLitter
     (φ.roughLitterMapOrElse_injOn_dom_inter_flexible hφ)
 
-theorem flexibleLitterLocalPerm_apply_eq {φ : NearLitterAction} {hφ : φ.Lawful} (L : Litter)
+theorem flexibleLitterPartialPerm_apply_eq {φ : NearLitterAction} {hφ : φ.Lawful} (L : Litter)
     (hL₁ : L ∈ φ.litterMap.Dom) (hL₂ : Flexible A L) :
-    φ.flexibleLitterLocalPerm hφ A L = φ.roughLitterMapOrElse L :=
-  LocalPerm.complete_apply_eq _ _ _ ⟨hL₁, hL₂⟩
+    φ.flexibleLitterPartialPerm hφ A L = φ.roughLitterMapOrElse L :=
+  PartialPerm.complete_apply_eq _ _ _ ⟨hL₁, hL₂⟩
 
-theorem flexibleLitterLocalPerm_domain_small (hφ : φ.Lawful) :
-    Small (φ.flexibleLitterLocalPerm hφ A).domain := by
+theorem flexibleLitterPartialPerm_domain_small (hφ : φ.Lawful) :
+    Small (φ.flexibleLitterPartialPerm hφ A).domain := by
   refine' Small.union (Small.union _ _) _
   · exact φ.litterMap_dom_small.mono (inter_subset_left _ _)
   · exact (φ.litterMap_dom_small.mono (inter_subset_left _ _)).image
   · rw [Small]
-    rw [Cardinal.mk_congr (LocalPerm.sandboxSubsetEquiv _ _)]
+    rw [Cardinal.mk_congr (PartialPerm.sandboxSubsetEquiv _ _)]
     simp only [mk_sum, mk_prod, mk_denumerable, lift_aleph0, lift_uzero, lift_id]
     refine' add_lt_of_lt Params.κ_isRegular.aleph0_le _ _ <;>
       refine' mul_lt_of_lt Params.κ_isRegular.aleph0_le

ConNF/FOA/Action/Refine.lean

@@ -100,12 +100,12 @@ theorem rc_smul_atom_eq {φ : StructAction β} {h : φ.Lawful} {B : ExtendedInde
   · simp only [refine_apply, refine_atomMap ha]
 
 theorem rc_smul_litter_eq {φ : StructAction β} {hφ : φ.Lawful} {B : ExtendedIndex β} (L : Litter) :
-    φ.rc hφ B • L = (φ.refine hφ B).flexibleLitterLocalPerm (refine_lawful B) B L :=
+    φ.rc hφ B • L = (φ.refine hφ B).flexibleLitterPartialPerm (refine_lawful B) B L :=
   rfl
 
 theorem rc_symm_smul_litter_eq {φ : StructAction β} {hφ : φ.Lawful} {B : ExtendedIndex β}
     (L : Litter) :
-    (φ.rc hφ B).symm • L = ((φ.refine hφ B).flexibleLitterLocalPerm (refine_lawful B) B).symm L :=
+    (φ.rc hφ B).symm • L = ((φ.refine hφ B).flexibleLitterPartialPerm (refine_lawful B) B).symm L :=
   rfl
 
 theorem rc_free (φ : StructAction β) (h₁ : φ.Lawful) (h₂ : φ.MapFlexible) :
@@ -114,7 +114,7 @@ theorem rc_free (φ : StructAction β) (h₁ : φ.Lawful) (h₂ : φ.MapFlexible
   · exact hL'.2
   · rw [NearLitterAction.roughLitterMapOrElse_of_dom _ hL'.1]
     exact h₂ B L' hL'.1 hL'.2
-  · exact (LocalPerm.sandboxSubset_subset _ _ hL').2
+  · exact (PartialPerm.sandboxSubset_subset _ _ hL').2
 
 theorem rc_comp_atomPerm {γ : Λ} {φ : StructAction β} {hφ : φ.Lawful}
     (A : Path (β : TypeIndex) γ) (B : ExtendedIndex γ) :

ConNF/FOA/Approximation/NearLitterApprox.lean

@@ -1,4 +1,4 @@
-import ConNF.Mathlib.Logic.Equiv.LocalPerm
+import ConNF.Mathlib.Logic.Equiv.PartialPerm
 import ConNF.FOA.Basic.Flexible
 import ConNF.FOA.Basic.Sublitter
 
@@ -18,8 +18,8 @@ variable [Params.{u}]
 
 @[ext]
 structure NearLitterApprox where
-  atomPerm : LocalPerm Atom
-  litterPerm : LocalPerm Litter
+  atomPerm : PartialPerm Atom
+  litterPerm : PartialPerm Litter
   domain_small : ∀ L, Small (litterSet L ∩ atomPerm.domain)
 
 namespace NearLitterApprox
@@ -39,26 +39,26 @@ theorem smul_litter_eq {L : Litter} : π.litterPerm L = π • L :=
   rfl
 
 @[simp]
-theorem mk_smul_atom {atomPerm : LocalPerm Atom} {litterPerm : LocalPerm Litter}
+theorem mk_smul_atom {atomPerm : PartialPerm Atom} {litterPerm : PartialPerm Litter}
     {domain_small : ∀ L, Small (litterSet L ∩ atomPerm.domain)} {a : Atom} :
     (⟨atomPerm, litterPerm, domain_small⟩ : NearLitterApprox) • a = atomPerm a :=
   rfl
 
 @[simp]
-theorem mk_smul_litter {atomPerm : LocalPerm Atom} {litterPerm : LocalPerm Litter}
+theorem mk_smul_litter {atomPerm : PartialPerm Atom} {litterPerm : PartialPerm Litter}
     {domain_small : ∀ L, Small (litterSet L ∩ atomPerm.domain)} {L : Litter} :
     (⟨atomPerm, litterPerm, domain_small⟩ : NearLitterApprox) • L = litterPerm L :=
   rfl
 
 theorem smul_eq_smul_atom {a₁ a₂ : Atom} (h₁ : a₁ ∈ π.atomPerm.domain)
     (h₂ : a₂ ∈ π.atomPerm.domain) : π • a₁ = π • a₂ ↔ a₁ = a₂ := by
   rw [mk_smul_atom, mk_smul_atom,
-    ← π.atomPerm.eq_symm_apply h₁ (π.atomPerm.map_domain h₂), LocalPerm.left_inv _ h₂]
+    ← π.atomPerm.eq_symm_apply h₁ (π.atomPerm.map_domain h₂), PartialPerm.left_inv _ h₂]
 
 theorem smul_eq_smul_litter {L₁ L₂ : Litter} (h₁ : L₁ ∈ π.litterPerm.domain)
     (h₂ : L₂ ∈ π.litterPerm.domain) : π • L₁ = π • L₂ ↔ L₁ = L₂ := by
   rw [mk_smul_litter, mk_smul_litter,
-    ← π.litterPerm.eq_symm_apply h₁ (π.litterPerm.map_domain h₂), LocalPerm.left_inv _ h₂]
+    ← π.litterPerm.eq_symm_apply h₁ (π.litterPerm.map_domain h₂), PartialPerm.left_inv _ h₂]
 
 def symm : NearLitterApprox where
   atomPerm := π.atomPerm.symm

ConNF/FOA/Basic/CompleteOrbit.lean

@@ -1,7 +1,7 @@
 import Mathlib.SetTheory.Cardinal.Ordinal
-import ConNF.Mathlib.Logic.Equiv.LocalPerm
+import ConNF.Mathlib.Logic.Equiv.PartialPerm
 
-namespace LocalPerm
+namespace PartialPerm
 
 /-!
 Utilities to complete orbits of functions into local permutations.
@@ -243,7 +243,7 @@ theorem complete_right_inv [Nonempty α] (hst : Disjoint (s ∪ f '' s) t) (hf :
 with domain contained in `s ∪ (f '' s) ∪ t`. -/
 noncomputable def complete [Nonempty α] (f : α → α) (s : Set α) (t : Set α)
     (hs : #(s ∆ (f '' s) : Set α) ≤ #t) (ht : ℵ₀ ≤ #t) (hst : Disjoint (s ∪ f '' s) t)
-    (hf : InjOn f s) : LocalPerm α
+    (hf : InjOn f s) : PartialPerm α
     where
   toFun := completeToFun hs ht
   invFun := completeInvFun hs ht
@@ -283,4 +283,4 @@ theorem complete_apply_eq (x : α) (hx : x ∈ s) : complete f s t hs ht hst hf
   exact fun h' => h'.2 hx
   exact not_mem_sandbox_of_mem hs ht hst x hx
 
-end LocalPerm
+end PartialPerm

ConNF/FOA/Complete/FlexibleCompletion.lean

@@ -13,7 +13,7 @@ variable [Params.{u}] [Level] [FOAAssumptions] {β : TypeIndex}
 
 namespace NearLitterApprox
 
-def idOnFlexible : LocalPerm Litter where
+def idOnFlexible : PartialPerm Litter where
   toFun := id
   invFun := id
   domain := {L | Flexible A L} \ π.litterPerm.domain
@@ -29,12 +29,12 @@ theorem idOnFlexible_domain :
 theorem idOnFlexible_domain_disjoint : Disjoint π.litterPerm.domain (idOnFlexible π A).domain :=
   by rw [disjoint_iff_inter_eq_empty, idOnFlexible_domain, inter_diff_self]
 
-noncomputable def flexibleCompletionLitterPerm : LocalPerm Litter :=
-  LocalPerm.piecewise π.litterPerm (idOnFlexible π A) (idOnFlexible_domain_disjoint π A)
+noncomputable def flexibleCompletionLitterPerm : PartialPerm Litter :=
+  PartialPerm.piecewise π.litterPerm (idOnFlexible π A) (idOnFlexible_domain_disjoint π A)
 
 theorem flexibleCompletionLitterPerm_domain :
     (flexibleCompletionLitterPerm π A).domain = π.litterPerm.domain ∪ {L | Flexible A L} := by
-  rw [flexibleCompletionLitterPerm, LocalPerm.piecewise_domain, idOnFlexible_domain,
+  rw [flexibleCompletionLitterPerm, PartialPerm.piecewise_domain, idOnFlexible_domain,
     union_diff_self]
 
 noncomputable def flexibleCompletion : NearLitterApprox
@@ -59,23 +59,23 @@ theorem flexibleCompletion_smul_eq (L : Litter) :
 theorem flexibleCompletion_smul_of_mem_domain (L : Litter) (hL : L ∈ π.litterPerm.domain) :
     flexibleCompletion π A • L = π.litterPerm L := by
   rw [flexibleCompletion_smul_eq, flexibleCompletionLitterPerm,
-    LocalPerm.piecewise_apply_eq_left hL]
+    PartialPerm.piecewise_apply_eq_left hL]
 
 theorem flexibleCompletion_smul_flexible (hπ : π.Free A) (L : Litter) (hL : Flexible A L) :
     Flexible A (flexibleCompletion π A • L) := by
-  have := LocalPerm.map_domain (flexibleCompletion π A).litterPerm (x := ?_) ?_
+  have := PartialPerm.map_domain (flexibleCompletion π A).litterPerm (x := ?_) ?_
   · rw [flexibleCompletion_litterPerm_domain_free π A hπ] at this
     exact this
   · rw [flexibleCompletion_litterPerm_domain_free π A hπ]
     exact hL
 
 theorem flexibleCompletion_symm_smul_flexible (hπ : π.Free A) (L : Litter) (hL : Flexible A L) :
     Flexible A ((flexibleCompletion π A).symm • L) := by
-  have := LocalPerm.map_domain (flexibleCompletion π A).symm.litterPerm (x := ?_) ?_
-  · rw [symm_litterPerm, LocalPerm.symm_domain,
+  have := PartialPerm.map_domain (flexibleCompletion π A).symm.litterPerm (x := ?_) ?_
+  · rw [symm_litterPerm, PartialPerm.symm_domain,
       flexibleCompletion_litterPerm_domain_free π A hπ] at this
     exact this
-  · rw [symm_litterPerm, LocalPerm.symm_domain,
+  · rw [symm_litterPerm, PartialPerm.symm_domain,
       flexibleCompletion_litterPerm_domain_free π A hπ]
     exact hL