diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean
index ba10664b5774..e8dbe7776f3a 100644
--- a/src/Init/Data/List.lean
+++ b/src/Init/Data/List.lean
@@ -21,3 +21,4 @@ import Init.Data.List.Pairwise
 import Init.Data.List.Sublist
 import Init.Data.List.TakeDrop
 import Init.Data.List.Zip
+import Init.Data.List.Perm
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 98bb6f30d79a..9df9667a6dbd 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -1223,6 +1223,36 @@ theorem lookup_cons [BEq α] {k : α} :
     ((k,b)::es).lookup a = match a == k with | true => some b | false => es.lookup a :=
   rfl
 
+/-! ## Permutations -/
+
+/-! ### Perm -/
+
+/--
+`Perm l₁ l₂` or `l₁ ~ l₂` asserts that `l₁` and `l₂` are permutations
+of each other. This is defined by induction using pairwise swaps.
+-/
+inductive Perm : List α → List α → Prop
+  /-- `[] ~ []` -/
+  | nil : Perm [] []
+  /-- `l₁ ~ l₂ → x::l₁ ~ x::l₂` -/
+  | cons (x : α) {l₁ l₂ : List α} : Perm l₁ l₂ → Perm (x :: l₁) (x :: l₂)
+  /-- `x::y::l ~ y::x::l` -/
+  | swap (x y : α) (l : List α) : Perm (y :: x :: l) (x :: y :: l)
+  /-- `Perm` is transitive. -/
+  | trans {l₁ l₂ l₃ : List α} : Perm l₁ l₂ → Perm l₂ l₃ → Perm l₁ l₃
+
+@[inherit_doc] scoped infixl:50 " ~ " => Perm
+
+/-! ### isPerm -/
+
+/--
+`O(|l₁| * |l₂|)`. Computes whether `l₁` is a permutation of `l₂`. See `isPerm_iff` for a
+characterization in terms of `List.Perm`.
+-/
+def isPerm [BEq α] : List α → List α → Bool
+  | [], l₂ => l₂.isEmpty
+  | a :: l₁, l₂ => l₂.contains a && l₁.isPerm (l₂.erase a)
+
 /-! ## Logical operations -/
 
 /-! ### any -/
diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
new file mode 100644
index 000000000000..788bafa57c11
--- /dev/null
+++ b/src/Init/Data/List/Perm.lean
@@ -0,0 +1,431 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
+prelude
+import Init.Data.List.Pairwise
+import Init.Data.List.Erase
+
+/-!
+# List Permutations
+
+This file introduces the `List.Perm` relation, which is true if two lists are permutations of one
+another.
+
+## Notation
+
+The notation `~` is used for permutation equivalence.
+-/
+
+open Nat
+
+namespace List
+
+open Perm (swap)
+
+@[simp, refl] protected theorem Perm.refl : ∀ l : List α, l ~ l
+  | [] => .nil
+  | x :: xs => (Perm.refl xs).cons x
+
+protected theorem Perm.rfl {l : List α} : l ~ l := .refl _
+
+theorem Perm.of_eq (h : l₁ = l₂) : l₁ ~ l₂ := h ▸ .rfl
+
+protected theorem Perm.symm {l₁ l₂ : List α} (h : l₁ ~ l₂) : l₂ ~ l₁ := by
+  induction h with
+  | nil => exact nil
+  | cons _ _ ih => exact cons _ ih
+  | swap => exact swap ..
+  | trans _ _ ih₁ ih₂ => exact trans ih₂ ih₁
+
+theorem perm_comm {l₁ l₂ : List α} : l₁ ~ l₂ ↔ l₂ ~ l₁ := ⟨Perm.symm, Perm.symm⟩
+
+theorem Perm.swap' (x y : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : y :: x :: l₁ ~ x :: y :: l₂ :=
+  (swap ..).trans <| p.cons _ |>.cons _
+
+/--
+Similar to `Perm.recOn`, but the `swap` case is generalized to `Perm.swap'`,
+where the tail of the lists are not necessarily the same.
+-/
+@[elab_as_elim] theorem Perm.recOnSwap'
+    {motive : (l₁ : List α) → (l₂ : List α) → l₁ ~ l₂ → Prop} {l₁ l₂ : List α} (p : l₁ ~ l₂)
+    (nil : motive [] [] .nil)
+    (cons : ∀ x {l₁ l₂}, (h : l₁ ~ l₂) → motive l₁ l₂ h → motive (x :: l₁) (x :: l₂) (.cons x h))
+    (swap' : ∀ x y {l₁ l₂}, (h : l₁ ~ l₂) → motive l₁ l₂ h →
+      motive (y :: x :: l₁) (x :: y :: l₂) (.swap' _ _ h))
+    (trans : ∀ {l₁ l₂ l₃}, (h₁ : l₁ ~ l₂) → (h₂ : l₂ ~ l₃) → motive l₁ l₂ h₁ → motive l₂ l₃ h₂ →
+      motive l₁ l₃ (.trans h₁ h₂)) : motive l₁ l₂ p :=
+  have motive_refl l : motive l l (.refl l) :=
+    List.recOn l nil fun x xs ih => cons x (.refl xs) ih
+  Perm.recOn p nil cons (fun x y l => swap' x y (.refl l) (motive_refl l)) trans
+
+theorem Perm.eqv (α) : Equivalence (@Perm α) := ⟨.refl, .symm, .trans⟩
+
+instance isSetoid (α) : Setoid (List α) := .mk Perm (Perm.eqv α)
+
+theorem Perm.mem_iff {a : α} {l₁ l₂ : List α} (p : l₁ ~ l₂) : a ∈ l₁ ↔ a ∈ l₂ := by
+  induction p with
+  | nil => rfl
+  | cons _ _ ih => simp only [mem_cons, ih]
+  | swap => simp only [mem_cons, or_left_comm]
+  | trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]
+
+theorem Perm.subset {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁ ⊆ l₂ := fun _ => p.mem_iff.mp
+
+theorem Perm.append_right {l₁ l₂ : List α} (t₁ : List α) (p : l₁ ~ l₂) : l₁ ++ t₁ ~ l₂ ++ t₁ := by
+  induction p with
+  | nil => rfl
+  | cons _ _ ih => exact cons _ ih
+  | swap => exact swap ..
+  | trans _ _ ih₁ ih₂ => exact trans ih₁ ih₂
+
+theorem Perm.append_left {t₁ t₂ : List α} : ∀ l : List α, t₁ ~ t₂ → l ++ t₁ ~ l ++ t₂
+  | [], p => p
+  | x :: xs, p => (p.append_left xs).cons x
+
+theorem Perm.append {l₁ l₂ t₁ t₂ : List α} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : l₁ ++ t₁ ~ l₂ ++ t₂ :=
+  (p₁.append_right t₁).trans (p₂.append_left l₂)
+
+theorem Perm.append_cons (a : α) {h₁ h₂ t₁ t₂ : List α} (p₁ : h₁ ~ h₂) (p₂ : t₁ ~ t₂) :
+    h₁ ++ a :: t₁ ~ h₂ ++ a :: t₂ := p₁.append (p₂.cons a)
+
+@[simp] theorem perm_middle {a : α} : ∀ {l₁ l₂ : List α}, l₁ ++ a :: l₂ ~ a :: (l₁ ++ l₂)
+  | [], _ => .refl _
+  | b :: _, _ => (Perm.cons _ perm_middle).trans (swap a b _)
+
+@[simp] theorem perm_append_singleton (a : α) (l : List α) : l ++ [a] ~ a :: l :=
+  perm_middle.trans <| by rw [append_nil]
+
+theorem perm_append_comm : ∀ {l₁ l₂ : List α}, l₁ ++ l₂ ~ l₂ ++ l₁
+  | [], l₂ => by simp
+  | a :: t, l₂ => (perm_append_comm.cons _).trans perm_middle.symm
+
+theorem perm_append_comm_assoc (l₁ l₂ l₃ : List α) :
+    Perm (l₁ ++ (l₂ ++ l₃)) (l₂ ++ (l₁ ++ l₃)) := by
+  simpa only [List.append_assoc] using perm_append_comm.append_right _
+
+theorem concat_perm (l : List α) (a : α) : concat l a ~ a :: l := by simp
+
+theorem Perm.length_eq {l₁ l₂ : List α} (p : l₁ ~ l₂) : length l₁ = length l₂ := by
+  induction p with
+  | nil => rfl
+  | cons _ _ ih => simp only [length_cons, ih]
+  | swap => rfl
+  | trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]
+
+theorem Perm.eq_nil {l : List α} (p : l ~ []) : l = [] := eq_nil_of_length_eq_zero p.length_eq
+
+theorem Perm.nil_eq {l : List α} (p : [] ~ l) : [] = l := p.symm.eq_nil.symm
+
+@[simp] theorem perm_nil {l₁ : List α} : l₁ ~ [] ↔ l₁ = [] :=
+  ⟨fun p => p.eq_nil, fun e => e ▸ .rfl⟩
+
+@[simp] theorem nil_perm {l₁ : List α} : [] ~ l₁ ↔ l₁ = [] := perm_comm.trans perm_nil
+
+@[simp]
+theorem not_perm_nil_cons (x : α) (l : List α) : ¬[] ~ x :: l := (nomatch ·.symm.eq_nil)
+
+@[simp]
+theorem not_perm_cons_nil {l : List α} {a : α} : ¬(Perm (a::l) []) :=
+  fun h => by simpa using h.length_eq
+
+theorem Perm.isEmpty_eq {l l' : List α} (h : Perm l l') : l.isEmpty = l'.isEmpty := by
+  cases l <;> cases l' <;> simp_all
+
+@[simp] theorem reverse_perm : ∀ l : List α, reverse l ~ l
+  | [] => .nil
+  | a :: l => reverse_cons .. ▸ (perm_append_singleton _ _).trans ((reverse_perm l).cons a)
+
+theorem perm_cons_append_cons {l l₁ l₂ : List α} (a : α) (p : l ~ l₁ ++ l₂) :
+    a :: l ~ l₁ ++ a :: l₂ := (p.cons a).trans perm_middle.symm
+
+@[simp] theorem perm_replicate {n : Nat} {a : α} {l : List α} :
+    l ~ replicate n a ↔ l = replicate n a := by
+  refine ⟨fun p => eq_replicate.2 ?_, fun h => h ▸ .rfl⟩
+  exact ⟨p.length_eq.trans <| length_replicate .., fun _b m => eq_of_mem_replicate <| p.subset m⟩
+
+@[simp] theorem replicate_perm {n : Nat} {a : α} {l : List α} :
+    replicate n a ~ l ↔ replicate n a = l := (perm_comm.trans perm_replicate).trans eq_comm
+
+@[simp] theorem perm_singleton {a : α} {l : List α} : l ~ [a] ↔ l = [a] := perm_replicate (n := 1)
+
+@[simp] theorem singleton_perm {a : α} {l : List α} : [a] ~ l ↔ [a] = l := replicate_perm (n := 1)
+
+theorem Perm.eq_singleton (h : l ~ [a]) : l = [a] := perm_singleton.mp h
+theorem Perm.singleton_eq (h : [a] ~ l) : [a] = l := singleton_perm.mp h
+
+theorem singleton_perm_singleton {a b : α} : [a] ~ [b] ↔ a = b := by simp
+
+theorem perm_cons_erase [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : l ~ a :: l.erase a :=
+  let ⟨_l₁, _l₂, _, e₁, e₂⟩ := exists_erase_eq h
+  e₂ ▸ e₁ ▸ perm_middle
+
+theorem Perm.filterMap (f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
+    filterMap f l₁ ~ filterMap f l₂ := by
+  induction p with
+  | nil => simp
+  | cons x _p IH => cases h : f x <;> simp [h, filterMap_cons, IH, Perm.cons]
+  | swap x y l₂ => cases hx : f x <;> cases hy : f y <;> simp [hx, hy, filterMap_cons, swap]
+  | trans _p₁ _p₂ IH₁ IH₂ => exact IH₁.trans IH₂
+
+theorem Perm.map (f : α → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) : map f l₁ ~ map f l₂ :=
+  filterMap_eq_map f ▸ p.filterMap _
+
+theorem Perm.pmap {p : α → Prop} (f : ∀ a, p a → β) {l₁ l₂ : List α} (p : l₁ ~ l₂) {H₁ H₂} :
+    pmap f l₁ H₁ ~ pmap f l₂ H₂ := by
+  induction p with
+  | nil => simp
+  | cons x _p IH => simp [IH, Perm.cons]
+  | swap x y => simp [swap]
+  | trans _p₁ p₂ IH₁ IH₂ => exact IH₁.trans (IH₂ (H₁ := fun a m => H₂ a (p₂.subset m)))
+
+theorem Perm.filter (p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) :
+    filter p l₁ ~ filter p l₂ := by rw [← filterMap_eq_filter]; apply s.filterMap
+
+theorem filter_append_perm (p : α → Bool) (l : List α) :
+    filter p l ++ filter (fun x => !p x) l ~ l := by
+  induction l with
+  | nil => rfl
+  | cons x l ih =>
+    by_cases h : p x <;> simp [h]
+    · exact ih.cons x
+    · exact Perm.trans (perm_append_comm.trans (perm_append_comm.cons _)) (ih.cons x)
+
+theorem exists_perm_sublist {l₁ l₂ l₂' : List α} (s : l₁ <+ l₂) (p : l₂ ~ l₂') :
+    ∃ l₁', l₁' ~ l₁ ∧ l₁' <+ l₂' := by
+  induction p generalizing l₁ with
+  | nil => exact ⟨[], sublist_nil.mp s ▸ .rfl, nil_sublist _⟩
+  | cons x _ IH =>
+    match s with
+    | .cons _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨l₁', p', s'.cons _⟩
+    | .cons₂ _ s => let ⟨l₁', p', s'⟩ := IH s; exact ⟨x :: l₁', p'.cons x, s'.cons₂ _⟩
+  | swap x y l' =>
+    match s with
+    | .cons _ (.cons _ s) => exact ⟨_, .rfl, (s.cons _).cons _⟩
+    | .cons _ (.cons₂ _ s) => exact ⟨x :: _, .rfl, (s.cons _).cons₂ _⟩
+    | .cons₂ _ (.cons _ s) => exact ⟨y :: _, .rfl, (s.cons₂ _).cons _⟩
+    | .cons₂ _ (.cons₂ _ s) => exact ⟨x :: y :: _, .swap .., (s.cons₂ _).cons₂ _⟩
+  | trans _ _ IH₁ IH₂ =>
+    let ⟨m₁, pm, sm⟩ := IH₁ s
+    let ⟨r₁, pr, sr⟩ := IH₂ sm
+    exact ⟨r₁, pr.trans pm, sr⟩
+
+theorem Perm.sizeOf_eq_sizeOf [SizeOf α] {l₁ l₂ : List α} (h : l₁ ~ l₂) :
+    sizeOf l₁ = sizeOf l₂ := by
+  induction h with
+  | nil => rfl
+  | cons _ _ h_sz₁₂ => simp [h_sz₁₂]
+  | swap => simp [Nat.add_left_comm]
+  | trans _ _ h_sz₁₂ h_sz₂₃ => simp [h_sz₁₂, h_sz₂₃]
+
+theorem Sublist.exists_perm_append {l₁ l₂ : List α} : l₁ <+ l₂ → ∃ l, l₂ ~ l₁ ++ l
+  | Sublist.slnil => ⟨nil, .rfl⟩
+  | Sublist.cons a s =>
+    let ⟨l, p⟩ := Sublist.exists_perm_append s
+    ⟨a :: l, (p.cons a).trans perm_middle.symm⟩
+  | Sublist.cons₂ a s =>
+    let ⟨l, p⟩ := Sublist.exists_perm_append s
+    ⟨l, p.cons a⟩
+
+theorem Perm.countP_eq (p : α → Bool) {l₁ l₂ : List α} (s : l₁ ~ l₂) :
+    countP p l₁ = countP p l₂ := by
+  simp only [countP_eq_length_filter]
+  exact (s.filter _).length_eq
+
+theorem Perm.countP_congr {l₁ l₂ : List α} (s : l₁ ~ l₂) {p p' : α → Bool}
+    (hp : ∀ x ∈ l₁, p x = p' x) : l₁.countP p = l₂.countP p' := by
+  rw [← s.countP_eq p']
+  clear s
+  induction l₁ with
+  | nil => rfl
+  | cons y s hs =>
+    simp only [mem_cons, forall_eq_or_imp] at hp
+    simp only [countP_cons, hs hp.2, hp.1]
+
+theorem countP_eq_countP_filter_add (l : List α) (p q : α → Bool) :
+    l.countP p = (l.filter q).countP p + (l.filter fun a => !q a).countP p :=
+  countP_append .. ▸ Perm.countP_eq _ (filter_append_perm _ _).symm
+
+theorem Perm.count_eq [DecidableEq α] {l₁ l₂ : List α} (p : l₁ ~ l₂) (a) :
+    count a l₁ = count a l₂ := p.countP_eq _
+
+theorem Perm.foldl_eq' {f : β → α → β} {l₁ l₂ : List α} (p : l₁ ~ l₂)
+    (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z), f (f z x) y = f (f z y) x)
+    (init) : foldl f init l₁ = foldl f init l₂ := by
+  induction p using recOnSwap' generalizing init with
+  | nil => simp
+  | cons x _p IH =>
+    simp only [foldl]
+    apply IH; intros; apply comm <;> exact .tail _ ‹_›
+  | swap' x y _p IH =>
+    simp only [foldl]
+    rw [comm x (.tail _ <| .head _) y (.head _)]
+    apply IH; intros; apply comm <;> exact .tail _ (.tail _ ‹_›)
+  | trans p₁ _p₂ IH₁ IH₂ =>
+    refine (IH₁ comm init).trans (IH₂ ?_ _)
+    intros; apply comm <;> apply p₁.symm.subset <;> assumption
+
+theorem Perm.rec_heq {β : List α → Sort _} {f : ∀ a l, β l → β (a :: l)} {b : β []} {l l' : List α}
+    (hl : l ~ l') (f_congr : ∀ {a l l' b b'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b'))
+    (f_swap : ∀ {a a' l b}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) :
+    HEq (@List.rec α β b f l) (@List.rec α β b f l') := by
+  induction hl with
+  | nil => rfl
+  | cons a h ih => exact f_congr h ih
+  | swap a a' l => exact f_swap
+  | trans _h₁ _h₂ ih₁ ih₂ => exact ih₁.trans ih₂
+
+/-- Lemma used to destruct perms element by element. -/
+theorem perm_inv_core {a : α} {l₁ l₂ r₁ r₂ : List α} :
+    l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂ := by
+  -- Necessary generalization for `induction`
+  suffices ∀ s₁ s₂ (_ : s₁ ~ s₂) {l₁ l₂ r₁ r₂},
+      l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂ from (this _ _ · rfl rfl)
+  intro s₁ s₂ p
+  induction p using Perm.recOnSwap' with intro l₁ l₂ r₁ r₂ e₁ e₂
+  | nil =>
+    simp at e₁
+  | cons x p IH =>
+    cases l₁ <;> cases l₂ <;>
+      dsimp at e₁ e₂ <;> injections <;> subst_vars
+    · exact p
+    · exact p.trans perm_middle
+    · exact perm_middle.symm.trans p
+    · exact (IH rfl rfl).cons _
+  | swap' x y p IH =>
+    obtain _ | ⟨y, _ | ⟨z, l₁⟩⟩ := l₁
+      <;> obtain _ | ⟨u, _ | ⟨v, l₂⟩⟩ := l₂
+      <;> dsimp at e₁ e₂ <;> injections <;> subst_vars
+      <;> try exact p.cons _
+    · exact (p.trans perm_middle).cons u
+    · exact ((p.trans perm_middle).cons _).trans (swap _ _ _)
+    · exact (perm_middle.symm.trans p).cons y
+    · exact (swap _ _ _).trans ((perm_middle.symm.trans p).cons u)
+    · exact (IH rfl rfl).swap' _ _
+  | trans p₁ p₂ IH₁ IH₂ =>
+    subst e₁ e₂
+    obtain ⟨l₂, r₂, rfl⟩ := append_of_mem (a := a) (p₁.subset (by simp))
+    exact (IH₁ rfl rfl).trans (IH₂ rfl rfl)
+
+theorem Perm.cons_inv {a : α} {l₁ l₂ : List α} : a :: l₁ ~ a :: l₂ → l₁ ~ l₂ :=
+  perm_inv_core (l₁ := []) (l₂ := [])
+
+@[simp] theorem perm_cons (a : α) {l₁ l₂ : List α} : a :: l₁ ~ a :: l₂ ↔ l₁ ~ l₂ :=
+  ⟨.cons_inv, .cons a⟩
+
+theorem perm_append_left_iff {l₁ l₂ : List α} : ∀ l, l ++ l₁ ~ l ++ l₂ ↔ l₁ ~ l₂
+  | [] => .rfl
+  | a :: l => (perm_cons a).trans (perm_append_left_iff l)
+
+theorem perm_append_right_iff {l₁ l₂ : List α} (l) : l₁ ++ l ~ l₂ ++ l ↔ l₁ ~ l₂ := by
+  refine ⟨fun p => ?_, .append_right _⟩
+  exact (perm_append_left_iff _).1 <| perm_append_comm.trans <| p.trans perm_append_comm
+
+section DecidableEq
+
+variable [DecidableEq α]
+
+theorem Perm.erase (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : l₁.erase a ~ l₂.erase a :=
+  if h₁ : a ∈ l₁ then
+    have h₂ : a ∈ l₂ := p.subset h₁
+    .cons_inv <| (perm_cons_erase h₁).symm.trans <| p.trans (perm_cons_erase h₂)
+  else by
+    have h₂ : a ∉ l₂ := mt p.mem_iff.2 h₁
+    rw [erase_of_not_mem h₁, erase_of_not_mem h₂]; exact p
+
+theorem cons_perm_iff_perm_erase {a : α} {l₁ l₂ : List α} :
+    a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a := by
+  refine ⟨fun h => ?_, fun ⟨m, h⟩ => (h.cons a).trans (perm_cons_erase m).symm⟩
+  have : a ∈ l₂ := h.subset (mem_cons_self a l₁)
+  exact ⟨this, (h.trans <| perm_cons_erase this).cons_inv⟩
+
+theorem perm_iff_count {l₁ l₂ : List α} : l₁ ~ l₂ ↔ ∀ a, count a l₁ = count a l₂ := by
+  refine ⟨Perm.count_eq, fun H => ?_⟩
+  induction l₁ generalizing l₂ with
+  | nil =>
+    match l₂ with
+    | nil => rfl
+    | cons b l₂ =>
+      specialize H b
+      simp at H
+  | cons a l₁ IH =>
+    have : a ∈ l₂ := count_pos_iff_mem.mp (by rw [← H]; simp)
+    refine ((IH fun b => ?_).cons a).trans (perm_cons_erase this).symm
+    specialize H b
+    rw [(perm_cons_erase this).count_eq] at H
+    by_cases h : b = a <;> simpa [h, count_cons, Nat.succ_inj'] using H
+
+theorem isPerm_iff : ∀ {l₁ l₂ : List α}, l₁.isPerm l₂ ↔ l₁ ~ l₂
+  | [], [] => by simp [isPerm, isEmpty]
+  | [], _ :: _ => by simp [isPerm, isEmpty, Perm.nil_eq]
+  | a :: l₁, l₂ => by simp [isPerm, isPerm_iff, cons_perm_iff_perm_erase]
+
+instance decidablePerm (l₁ l₂ : List α) : Decidable (l₁ ~ l₂) := decidable_of_iff _ isPerm_iff
+
+protected theorem Perm.insert (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
+    l₁.insert a ~ l₂.insert a := by
+  if h : a ∈ l₁ then
+    simp [h, p.subset h, p]
+  else
+    have := p.cons a
+    simpa [h, mt p.mem_iff.2 h] using this
+
+theorem perm_insert_swap (x y : α) (l : List α) :
+    List.insert x (List.insert y l) ~ List.insert y (List.insert x l) := by
+  by_cases xl : x ∈ l <;> by_cases yl : y ∈ l <;> simp [xl, yl]
+  if xy : x = y then simp [xy] else
+  simp [List.insert, xl, yl, xy, Ne.symm xy]
+  constructor
+
+end DecidableEq
+
+theorem Perm.pairwise_iff {R : α → α → Prop} (S : ∀ {x y}, R x y → R y x) :
+    ∀ {l₁ l₂ : List α} (_p : l₁ ~ l₂), Pairwise R l₁ ↔ Pairwise R l₂ :=
+  suffices ∀ {l₁ l₂}, l₁ ~ l₂ → Pairwise R l₁ → Pairwise R l₂
+    from fun p => ⟨this p, this p.symm⟩
+  fun {l₁ l₂} p d => by
+    induction d generalizing l₂ with
+    | nil => rw [← p.nil_eq]; constructor
+    | cons h _ IH =>
+      have : _ ∈ l₂ := p.subset (mem_cons_self _ _)
+      obtain ⟨s₂, t₂, rfl⟩ := append_of_mem this
+      have p' := (p.trans perm_middle).cons_inv
+      refine (pairwise_middle S).2 (pairwise_cons.2 ⟨fun b m => ?_, IH p'⟩)
+      exact h _ (p'.symm.subset m)
+
+theorem Pairwise.perm {R : α → α → Prop} {l l' : List α} (hR : l.Pairwise R) (hl : l ~ l')
+    (hsymm : ∀ {x y}, R x y → R y x) : l'.Pairwise R := (hl.pairwise_iff hsymm).mp hR
+
+theorem Perm.pairwise {R : α → α → Prop} {l l' : List α} (hl : l ~ l') (hR : l.Pairwise R)
+    (hsymm : ∀ {x y}, R x y → R y x) : l'.Pairwise R := hR.perm hl hsymm
+
+theorem Perm.nodup_iff {l₁ l₂ : List α} : l₁ ~ l₂ → (Nodup l₁ ↔ Nodup l₂) :=
+  Perm.pairwise_iff <| @Ne.symm α
+
+theorem Perm.join {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.join ~ l₂.join := by
+  induction h with
+  | nil => rfl
+  | cons _ _ ih => simp only [join_cons, perm_append_left_iff, ih]
+  | swap => simp only [join_cons, ← append_assoc, perm_append_right_iff]; exact perm_append_comm ..
+  | trans _ _ ih₁ ih₂ => exact trans ih₁ ih₂
+
+theorem Perm.bind_right {l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.bind f ~ l₂.bind f :=
+  (p.map _).join
+
+theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
+    (H : Pairwise (fun a b => f a → f b → False) l₁) (p : l₁ ~ l₂) : eraseP f l₁ ~ eraseP f l₂ := by
+  induction p with
+  | nil => simp
+  | cons a p IH =>
+    if h : f a then simp [h, p]
+    else simp [h]; exact IH (pairwise_cons.1 H).2
+  | swap a b l =>
+    by_cases h₁ : f a <;> by_cases h₂ : f b <;> simp [h₁, h₂]
+    · cases (pairwise_cons.1 H).1 _ (mem_cons.2 (Or.inl rfl)) h₂ h₁
+    · apply swap
+  | trans p₁ _ IH₁ IH₂ =>
+    refine (IH₁ H).trans (IH₂ ((p₁.pairwise_iff ?_).1 H))
+    exact fun h h₁ h₂ => h h₂ h₁
+
+end List
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
index a3e530b1023a..9db1c5de8985 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
@@ -18,6 +18,7 @@ set_option linter.missingDocs true
 set_option autoImplicit false
 
 open Std.DHashMap.Internal
+open List (Perm perm_middle)
 
 universe w v u
 
@@ -133,15 +134,15 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} {l : AssocLis
     simpa using this .nil l
   intros l l'
   induction l' generalizing l
-  · simpa [filterMap.go] using Perm.refl _
+  · simp [filterMap.go]
   · next k v t ih =>
     simp only [filterMap.go, toList_cons, List.filterMap_cons]
     split
-    · next h => exact (ih _).trans (by simpa [h] using Perm.refl _)
+    · next h => exact (ih _).trans (by simp [h])
     · next h =>
       refine (ih _).trans ?_
       simp only [toList_cons, List.cons_append]
-      exact perm_middle.symm.trans (by simpa [h] using Perm.refl _)
+      exact perm_middle.symm.trans (by simp [h])
 
 theorem toList_map {f : (a : α) → β a → γ a} {l : AssocList α β} :
     Perm (l.map f).toList (l.toList.map fun p => ⟨p.1, f p.1 p.2⟩) := by
@@ -151,7 +152,7 @@ theorem toList_map {f : (a : α) → β a → γ a} {l : AssocList α β} :
     simpa using this .nil l
   intros l l'
   induction l' generalizing l
-  · simpa [map.go] using Perm.refl _
+  · simp [map.go]
   · next k v t ih =>
     simp only [map.go, toList_cons, List.map_cons]
     refine (ih _).trans ?_
@@ -165,7 +166,7 @@ theorem toList_filter {f : (a : α) → β a → Bool} {l : AssocList α β} :
     simpa using this .nil l
   intros l l'
   induction l' generalizing l
-  · simpa [filter.go] using Perm.refl _
+  · simp [filter.go]
   · next k v t ih =>
     simp only [filter.go, toList_cons, List.filter_cons, cond_eq_if]
     split
diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 9de800657c69..c829b607fa73 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -22,6 +22,8 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {γ : α → Type w}
 
+open List (Perm)
+
 namespace Std.DHashMap.Internal.List
 
 @[elab_as_elim]
@@ -1340,16 +1342,16 @@ theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) 
     (hl : DistinctKeys l) (h : Perm l l') : getEntry? a l = getEntry? a l' := by
   induction h
   · simp
-  · next t₁ t₂ p _ ih₂ =>
+  · next p t₁ t₂ _ ih₂ =>
     rcases p with ⟨k', v'⟩
     simp only [getEntry?_cons, ih₂ hl.tail]
-  · next p p' _ _ =>
+  · next p p' _ =>
     rcases p with ⟨k₁, v₁⟩
     rcases p' with ⟨k₂, v₂⟩
     simp only [getEntry?_cons]
     cases h₂ : k₂ == a <;> cases h₁ : k₁ == a <;> try simp; done
     simp only [distinctKeys_cons_iff, containsKey_cons, Bool.or_eq_false_iff] at hl
-    exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₂ (BEq.symm h₁))).elim
+    exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₁ (BEq.symm h₂))).elim
   · next l₁ l₂ l₃ hl₁₂ _ ih₁ ih₂ => exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm)))
 
 theorem containsKey_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α}
@@ -1417,8 +1419,8 @@ theorem perm_cons_getEntry [BEq α] {l : List ((a : α) × β a)} {a : α} (h :
     cases hk : k' == a
     · obtain ⟨l', hl'⟩ := ih (h.resolve_left (Bool.not_eq_true _ ▸ hk))
       rw [getEntry_cons_of_false hk]
-      exact ⟨⟨k', v'⟩ :: l', (hl'.cons _).trans (Perm.swap _ _ (Perm.refl _))⟩
-    · exact ⟨t, by rw [getEntry_cons_of_beq hk]; exact Perm.refl _⟩
+      exact ⟨⟨k', v'⟩ :: l', (hl'.cons _).trans (Perm.swap' _ _ (Perm.refl _))⟩
+    · exact ⟨t, by rw [getEntry_cons_of_beq hk]⟩
 
 -- Note: this theorem becomes false if you don't assume that BEq is reflexive on α.
 theorem getEntry?_ext [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} (hl : DistinctKeys l)
diff --git a/src/Std/Data/DHashMap/Internal/List/Pairwise.lean b/src/Std/Data/DHashMap/Internal/List/Pairwise.lean
index 17f315104531..38455e818a28 100644
--- a/src/Std/Data/DHashMap/Internal/List/Pairwise.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Pairwise.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 prelude
+import Init.Data.List.Perm
 import Std.Data.DHashMap.Internal.List.Defs
-import Std.Data.DHashMap.Internal.List.Perm
 import Std.Data.DHashMap.Internal.List.Sublist
 
 /-!
@@ -18,6 +18,8 @@ File contents: tiny private implementation of `List.Pairwise`
 set_option linter.missingDocs true
 set_option autoImplicit false
 
+open List (Perm)
+
 namespace Std.DHashMap.Internal.List
 
 
@@ -34,7 +36,7 @@ theorem Pairwise.perm {P : α → α → Prop} (hP : ∀ {x y}, P x y → P y x)
   induction h
   · exact id
   · next l₁ l₂ a h ih => exact fun hx => ⟨fun y hy => hx.1 _ (h.mem_iff.2 hy), ih hx.2⟩
-  · next l₁ _ a a' _ _ =>
+  · next l₁ a a' =>
     intro ⟨hx₁, hx₂, hx⟩
     refine ⟨?_, ?_, hx⟩
     · intro y hy
diff --git a/src/Std/Data/DHashMap/Internal/List/Perm.lean b/src/Std/Data/DHashMap/Internal/List/Perm.lean
deleted file mode 100644
index c5bc1faa9b2d..000000000000
--- a/src/Std/Data/DHashMap/Internal/List/Perm.lean
+++ /dev/null
@@ -1,106 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-prelude
-import Init.Data.List.Lemmas
-
-/-!
-This is an internal implementation file of the hash map. Users of the hash map should not rely on
-the contents of this file.
-
-File contents: tiny private implementation of `List.Perm`
--/
-
-set_option linter.missingDocs true
-set_option autoImplicit false
-
-universe u v
-
-variable {α : Type u} {β : Type v}
-
-namespace Std.DHashMap.Internal.List
-
-/-- Internal implementation detail of the hash map -/
-inductive Perm : List α → List α → Prop where
-  /-- Internal implementation detail of the hash map -/
-  | refl (l) : Perm l l
-  /-- Internal implementation detail of the hash map -/
-  | cons {l l'} (a) : Perm l l' → Perm (a::l) (a::l')
-  /-- Internal implementation detail of the hash map -/
-  | swap {l l'} (a b) : Perm l l' → Perm (a::b::l) (b::a::l)
-  /-- Internal implementation detail of the hash map -/
-  | trans {l l' l''} : Perm l l' → Perm l' l'' → Perm l l''
-
-theorem Perm.append_right {l₁ l₂ : List α} (l₃ : List α) (h : Perm l₁ l₂) :
-    Perm (l₁ ++ l₃) (l₂ ++ l₃) := by
-  induction h
-  · exact .refl _
-  · next a _ ih => exact .cons a ih
-  · next a b _ ih => exact .swap a b ih
-  · next ih₁ ih₂ => exact .trans ih₁ ih₂
-
-theorem Perm.symm {l₁ l₂ : List α} (h : Perm l₁ l₂) : Perm l₂ l₁ := by
-  induction h
-  · exact .refl _
-  · exact .cons _ ‹_›
-  · exact .swap _ _ ‹_›
-  · next ih₁ ih₂ => exact .trans ih₂ ih₁
-
-theorem perm_middle {l₁ l₂ : List α} {a : α} : Perm (l₁ ++ a :: l₂) (a :: (l₁ ++ l₂)) := by
-  induction l₁
-  · simpa using .refl _
-  · next h t ih => exact .trans (.cons _ ih) (.swap _ _ (.refl _))
-
-theorem perm_append_comm {l₁ l₂ : List α} : Perm (l₁ ++ l₂) (l₂ ++ l₁) := by
-  induction l₁ generalizing l₂
-  · simpa using .refl _
-  · next h t ih => exact .trans (.cons _ ih) (Perm.symm perm_middle)
-
-theorem Perm.append_left (l₁ : List α) {l₂ l₃ : List α} (h : Perm l₂ l₃) :
-    Perm (l₁ ++ l₂) (l₁ ++ l₃) :=
-  Perm.trans perm_append_comm (Perm.trans (Perm.append_right _ h) perm_append_comm)
-
-theorem Perm.append {l₁ l₂ l₃ l₄ : List α} (h₁ : Perm l₁ l₂) (h₂ : Perm l₃ l₄) :
-    Perm (l₁ ++ l₃) (l₂ ++ l₄) :=
-  Perm.trans (Perm.append_right l₃ h₁)
-    (Perm.trans perm_append_comm (Perm.trans (Perm.append_right _ h₂) perm_append_comm))
-
-theorem Perm.length_eq {l l' : List α} (h : Perm l l') : l.length = l'.length := by
-  induction h <;> simp_all
-
-@[simp]
-theorem not_perm_empty_cons {l : List α} {a : α} : ¬(Perm [] (a::l)) :=
-  fun h => by simpa using h.length_eq
-
-@[simp]
-theorem not_perm_cons_empty {l : List α} {a : α} : ¬(Perm (a::l) []) :=
-  fun h => by simpa using h.length_eq
-
-theorem Perm.isEmpty_eq {l l' : List α} (h : Perm l l') : l.isEmpty = l'.isEmpty := by
-  cases l <;> cases l' <;> simp_all
-
-theorem perm_append_comm_assoc (l₁ l₂ l₃ : List α) :
-    Perm (l₁ ++ (l₂ ++ l₃)) (l₂ ++ (l₁ ++ l₃)) := by
-  simpa only [List.append_assoc] using perm_append_comm.append_right _
-
-theorem Perm.mem_iff {l₁ l₂ : List α} (h : Perm l₁ l₂) {a : α} : a ∈ l₁ ↔ a ∈ l₂ := by
-  induction h <;> simp_all [← or_assoc, Or.comm]
-
-theorem Perm.map (f : α → β) {l₁ l₂ : List α} (h : Perm l₁ l₂) : Perm (l₁.map f) (l₂.map f) := by
-  induction h
-  · exact .refl _
-  · exact .cons _ ‹_›
-  · exact .swap _ _ ‹_›
-  · exact .trans ‹_› ‹_›
-
-theorem reverse_perm {l : List α} : Perm l.reverse l := by
-  induction l
-  · simpa using .refl _
-  · next h t ih =>
-    rw [List.reverse_cons]
-    refine Perm.trans perm_append_comm ?_
-    simpa only [List.singleton_append] using Perm.cons _ ih
-
-end Std.DHashMap.Internal.List
diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean
index ce0e6f023d26..fd95bc4b5190 100644
--- a/src/Std/Data/DHashMap/Internal/Model.lean
+++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -27,6 +27,8 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {γ : Type w} {δ : α → Type w}
 
+open List (Perm perm_append_comm_assoc)
+
 namespace Std.DHashMap.Internal
 
 open Internal.List
@@ -170,8 +172,7 @@ theorem toListModel_updateBucket [BEq α] [Hashable α] [PartialEquivBEq α] [La
   obtain ⟨l, h₁, h₂, h₃⟩ := exists_bucket_of_update m.1.buckets m.2 a f
   refine h₂.trans (Perm.trans ?_ (hg₁ hm.distinct h₁).symm)
   rw [hfg, hg₂]
-  · exact Perm.refl _
-  · exact h₃ hm.buckets_hash_self _ rfl
+  exact h₃ hm.buckets_hash_self _ rfl
 
 /-- This is the general theorem to show that mapping operations (like `map` and `filter`) are
 correct. -/
@@ -191,7 +192,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
       Perm (g l'') l' →
       Perm (l.foldl (fun acc a => acc ++ (f a).toList) l')
         (g (l.foldl (fun acc a => acc ++ a.toList) l'')) by
-    simpa using this m.1.buckets.data [] [] (by simpa [hg₀] using Perm.refl _)
+    simpa using this m.1.buckets.data [] [] (by simp [hg₀])
   rintro l l' l'' h
   induction l generalizing l' l''
   · simpa using h.symm
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 73d33cde2cd7..1232ab8a5497 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -89,8 +89,8 @@ private def modifyNames : Array Name :=
   #[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew]
 
 private def congrNames : MacroM (Array (TSyntax `term)) := do
-  return #[← `(Std.DHashMap.Internal.List.Perm.isEmpty_eq), ← `(containsKey_of_perm),
-    ← `(Std.DHashMap.Internal.List.Perm.length_eq), ← `(getValueCast?_of_perm _),
+  return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm),
+    ← `(_root_.List.Perm.length_eq), ← `(getValueCast?_of_perm _),
     ← `(getValue?_of_perm _), ← `(getValue_of_perm _), ← `(getValueCast_of_perm _),
     ← `(getValueCast!_of_perm _), ← `(getValueCastD_of_perm _), ← `(getValue!_of_perm _),
     ← `(getValueD_of_perm _) ]
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 84e3dfac515c..989d6a6cbc49 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -91,8 +91,7 @@ theorem toListModel_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α]
     Perm (toListModel (reinsertAux hash data a b).1) (⟨a, b⟩ :: toListModel data.1) := by
   rw [reinsertAux_eq]
   obtain ⟨l, h₁, h₂, -⟩ := exists_bucket_of_update data.1 data.2 a (fun l => l.cons a b)
-  refine h₂.trans ?_
-  simpa using Perm.cons _ (Perm.symm h₁)
+  exact h₂.trans (Perm.cons _ (Perm.symm h₁))
 
 theorem isHashSelf_foldl_reinsertAux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
     (l : List ((a : α) × β a)) (target : { d : Array (AssocList α β) // 0 < d.size }) :
@@ -107,7 +106,7 @@ theorem toListModel_foldl_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α
     Perm (toListModel (l.foldl (fun acc p => reinsertAux hash acc p.1 p.2) target).1)
       (l ++ toListModel target.1) := by
   induction l generalizing target
-  · simpa using Perm.refl _
+  · simp
   · next k v t ih =>
     simp only [foldl_cons, cons_append]
     refine (ih _).trans ?_
@@ -480,8 +479,7 @@ theorem toListModel_perm_eraseKey_of_containsₘ_eq_false [BEq α] [Hashable α]
     [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.1) (h' : m.containsₘ a = false) :
     Perm (toListModel m.1.buckets) (eraseKey a (toListModel m.1.buckets)) := by
   rw [eraseKey_of_containsKey_eq_false]
-  · exact Perm.refl _
-  · rw [← containsₘ_eq_containsKey h, h']
+  rw [← containsₘ_eq_containsKey h, h']
 
 theorem toListModel_eraseₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
     {a : α} (h : Raw.WFImp m.1) :
@@ -518,7 +516,7 @@ theorem toListModel_filterMapₘ {m : Raw₀ α β} {f : (a : α) → β a → O
     Perm (toListModel (m.filterMapₘ f).1.buckets)
       ((toListModel m.1.buckets).filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) :=
   toListModel_updateAllBuckets AssocList.toList_filterMap
-    (by simp [List.filterMap_append]; exact Perm.refl _)
+    (by simp [List.filterMap_append])
 
 theorem isHashSelf_filterMapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
     {f : (a : α) → β a → Option (δ a)} (h : Raw.WFImp m.1) :
@@ -554,7 +552,7 @@ theorem wfImp_filterMap [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
 theorem toListModel_mapₘ {m : Raw₀ α β} {f : (a : α) → β a → δ a} :
     Perm (toListModel (m.mapₘ f).1.buckets)
       ((toListModel m.1.buckets).map fun p => ⟨p.1, f p.1 p.2⟩) :=
-  toListModel_updateAllBuckets AssocList.toList_map (by simp; exact Perm.refl _)
+  toListModel_updateAllBuckets AssocList.toList_map (by simp)
 
 theorem isHashSelf_mapₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
     {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : IsHashSelf (m.mapₘ f).1.buckets := by
@@ -587,7 +585,7 @@ theorem wfImp_map [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m :
 theorem toListModel_filterₘ {m : Raw₀ α β} {f : (a : α) → β a → Bool} :
     Perm (toListModel (m.filterₘ f).1.buckets)
       ((toListModel m.1.buckets).filter fun p => f p.1 p.2) :=
-  toListModel_updateAllBuckets AssocList.toList_filter (by simp; exact Perm.refl _)
+  toListModel_updateAllBuckets AssocList.toList_filter (by simp)
 
 theorem isHashSelf_filterₘ [BEq α] [Hashable α] [ReflBEq α] [LawfulHashable α] {m : Raw₀ α β}
     {f : (a : α) → β a → Bool} (h : Raw.WFImp m.1) : IsHashSelf (m.filterₘ f).1.buckets := by
diff --git a/tests/lean/run/constructor_as_variable.lean b/tests/lean/run/constructor_as_variable.lean
index ffc831ec1ce1..d594702a1d2d 100644
--- a/tests/lean/run/constructor_as_variable.lean
+++ b/tests/lean/run/constructor_as_variable.lean
@@ -101,7 +101,13 @@ def ctorSuggestion1 (pair : MyProd) : Nat :=
 error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
 
 Suggestions:
-  'List.Pairwise.below.cons', 'List.Pairwise.cons', 'List.Sublist.below.cons', 'List.Sublist.cons', 'List.cons'
+  'List.Pairwise.below.cons',
+  'List.Pairwise.cons',
+  'List.Perm.below.cons',
+  'List.Perm.cons',
+  'List.Sublist.below.cons',
+  'List.Sublist.cons',
+  'List.cons'
 ---
 warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
 note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
@@ -123,6 +129,8 @@ error: invalid pattern, constructor or constant marked with '[match_pattern]' ex
 Suggestions:
   'List.Pairwise.below.cons',
   'List.Pairwise.cons',
+  'List.Perm.below.cons',
+  'List.Perm.cons',
   'List.Sublist.below.cons',
   'List.Sublist.cons',
   'List.cons',