diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index a69445f0144109..49a5d26c9ae6ed 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -43,66 +43,106 @@ section AdmissibleLists
 
 variable (m : ℕ)
 /-- A list of natural numbers `[i₀, ⋯, iₙ]` is said to be `m`-admissible (for `m : ℕ`) if
-`i₀ < ⋯ < iₙ` and `iₖ ≤ m + k` for all `k`.
+`i₀ < ⋯ < iₙ` and `iₖ ≤ m + k` for all `k`. This would suggest the definition
+`L.IsChain (· < ·) ∧ ∀ k, (h : k < L.length) → L[k] ≤ m + k`.
+However, we instead define `IsAdmissible` inductively and show, in
+`isAdmissible_iff_isChain_and_le`, that this is equivalent to the non-inductive definition.
 -/
-def IsAdmissible (L : List ℕ) : Prop :=
-  List.Sorted (· < ·) L ∧
-  ∀ (k : ℕ), (h : k < L.length) → L[k] ≤ m + k
+@[mk_iff]
+inductive IsAdmissible : (m : ℕ) → (L : List ℕ) → Prop
+  | nil (m : ℕ) : IsAdmissible m []
+  | singleton {m a} (ha : a ≤ m) : IsAdmissible m [a]
+  | cons_cons {m a b L'} (hab : a < b) (hbL : IsAdmissible (m + 1) (b :: L'))
+      (ha : a ≤ m) : IsAdmissible m (a :: b :: L')
+
+attribute [simp, grind ←] IsAdmissible.nil
+attribute [grind →] IsAdmissible.singleton
+attribute [grind →] IsAdmissible.cons_cons
+
+section IsAdmissible
+
+variable {m a b : ℕ} {L : List ℕ}
+
+@[simp, grind =]
+theorem isAdmissible_singleton_iff : IsAdmissible m [a] ↔ a ≤ m :=
+  ⟨fun | .singleton h => h, .singleton⟩
+
+@[simp, grind =]
+theorem isAdmissible_cons_cons_iff : IsAdmissible m (a :: b :: L) ↔
+    a < b ∧ IsAdmissible (m + 1) (b :: L) ∧ a ≤ m :=
+  ⟨fun | .cons_cons hab hbL ha => ⟨hab, hbL, ha⟩, by grind⟩
+
+theorem isAdmissible_cons_iff : IsAdmissible m (a :: L) ↔
+    a ≤ m ∧ ((_ : 0 < L.length) → a < L[0]) ∧ IsAdmissible (m + 1) L := by
+  cases L <;> grind
+
+theorem isAdmissible_iff_isChain_and_le : IsAdmissible m L ↔
+    L.IsChain (· < ·) ∧ ∀ k, (h : k < L.length) → L[k] ≤ m + k := by
+  induction L using List.twoStepInduction generalizing m with
+  | nil => grind
+  | singleton _ => simp
+  | cons_cons _ _ _ _ IH =>
+    simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
+      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
+    exact fun _ _ => ⟨fun h => by grind,
+      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩
+
+theorem isAdmissible_iff_pairwise_and_le : IsAdmissible m L ↔
+    L.Pairwise (· < ·) ∧ ∀ k, (h : k < L.length) → L[k] ≤ m + k := by
+  rw [isAdmissible_iff_isChain_and_le, List.isChain_iff_pairwise]
+
+theorem isAdmissible_of_isChain_of_forall_getElem_le {m L} (hL : L.IsChain (· < ·))
+    (hL₂ : ∀ k, (h : k < L.length) → L[k] ≤ m + k) : IsAdmissible m L :=
+  isAdmissible_iff_isChain_and_le.mpr ⟨hL, hL₂⟩
 
 namespace IsAdmissible
 
-lemma nil : IsAdmissible m [] := by simp [IsAdmissible]
+@[grind →] theorem isChain {m L} (hL : IsAdmissible m L) :
+    L.IsChain (· < ·) := (isAdmissible_iff_isChain_and_le.mp hL).1
 
-variable {m}
+@[grind →] theorem le {m} {L : List ℕ} (hL : IsAdmissible m L) : ∀ k (h : k < L.length),
+    L[k] ≤ m + k := (isAdmissible_iff_isChain_and_le.mp hL).2
+
+/-- The tail of an `m`-admissible list is (m+1)-admissible. -/
+@[grind →] lemma of_cons {m a L} (h : IsAdmissible m (a :: L)) :
+    IsAdmissible (m + 1) L := by cases L <;> grind
 
-lemma sorted {L : List ℕ} (hL : IsAdmissible m L) : L.Sorted (· < ·) := hL.1
+@[deprecated (since := "2025-10-15")]
+alias tail := IsAdmissible.of_cons
 
-lemma le {L : List ℕ} (hL : IsAdmissible m L) : ∀ (k : ℕ), (h : k < L.length) → L[k] ≤ m + k := hL.2
+lemma cons {m a L} (hL : IsAdmissible (m + 1) L) (ha : a ≤ m)
+    (ha' : (_ : 0 < L.length) → a < L[0]) : IsAdmissible m (a :: L) := by cases L <;> grind
+
+theorem pairwise {m L} (hL : IsAdmissible m L) : L.Pairwise (· < ·) :=
+  hL.isChain.pairwise
+
+@[deprecated  (since := "2025-10-16")]
+alias sorted := pairwise
 
 /-- If `(a :: l)` is `m`-admissible then a is less than all elements of `l` -/
-lemma head_lt (a : ℕ) (L : List ℕ) (hl : IsAdmissible m (a :: L)) :
-    ∀ a' ∈ L, a < a' := fun i hi ↦ (List.sorted_cons.mp hl.sorted).left i hi
-
-/-- If `L` is a `(m + 1)`-admissible list, and `a` is natural number such that a ≤ m and a < L[0],
-then `a::L` is `m`-admissible -/
-lemma cons (L : List ℕ) (hL : IsAdmissible (m + 1) L) (a : ℕ) (ha : a ≤ m)
-    (ha' : (_ : 0 < L.length) → a < L[0]) : IsAdmissible m (a :: L) := by
-  cases L with
-  | nil => constructor <;> simp [ha]
-  | cons head tail =>
-    simp only [List.length_cons, lt_add_iff_pos_left, add_pos_iff,
-      Nat.lt_one_iff, pos_of_gt, or_true, List.getElem_cons_zero,
-      forall_const] at ha'
-    simp only [IsAdmissible, List.sorted_cons, List.mem_cons, forall_eq_or_imp]
-    constructor <;> repeat constructor
-    · exact ha'
-    · rw [← List.forall_getElem]
-      intro i hi
-      exact ha'.trans <| (List.sorted_cons.mp hL.sorted).left tail[i] <| List.getElem_mem hi
-    · exact List.sorted_cons.mp hL.sorted
-    · rintro ⟨_ | _⟩ hi
-      · simp [ha]
-      · haveI := hL.le _ <| Nat.lt_of_succ_lt_succ hi
-        rw [List.getElem_cons_succ]
-        cutsat
+@[grind →]
+lemma head_lt {m a L} (hL : IsAdmissible m (a :: L)) :
+    ∀ a' ∈ L, a < a' := fun _ => L.rel_of_pairwise_cons hL.pairwise
 
-/-- The tail of an `m`-admissible list is (m+1)-admissible. -/
-lemma tail (a : ℕ) (l : List ℕ) (h : IsAdmissible m (a::l)) :
-    IsAdmissible (m + 1) l := by
-  refine ⟨(List.sorted_cons.mp h.sorted).right, ?_⟩
-  intro k _
-  simpa [Nat.add_assoc, Nat.add_comm 1] using h.le (k + 1) (by simpa)
+@[grind →] lemma getElem_lt {m L} (hL : IsAdmissible m L)
+    {k : ℕ} {hk : k < L.length} : L[k] < m + L.length :=
+  (hL.le k hk).trans_lt (Nat.add_lt_add_left hk _)
 
 /-- An element of a `m`-admissible list, as an element of the appropriate `Fin` -/
 @[simps]
-def getElemAsFin {L : List ℕ} (hl : IsAdmissible m L) (k : ℕ)
+def getElemAsFin {m L} (hl : IsAdmissible m L) (k : ℕ)
     (hK : k < L.length) : Fin (m + k + 1) :=
-  Fin.mk L[k] <| Nat.le_iff_lt_add_one.mp (by simp [hl.le])
+  Fin.mk L[k] <| Nat.le_iff_lt_add_one.mp (by grind)
 
 /-- The head of an `m`-admissible list. -/
 @[simps!]
-def head (a : ℕ) (L : List ℕ) (hl : IsAdmissible m (a :: L)) : Fin (m + 1) :=
-  hl.getElemAsFin 0 (by simp)
+def head {m a L} (hl : IsAdmissible m (a :: L)) : Fin (m + 1) :=
+  hl.getElemAsFin 0 (by grind)
+
+theorem mono {n} (hmn : m ≤ n) (hL : IsAdmissible m L) : IsAdmissible n L :=
+  isAdmissible_of_isChain_of_forall_getElem_le (by grind) (by grind)
+
+end IsAdmissible
 
 end IsAdmissible
 
@@ -114,6 +154,7 @@ satisfying `P_σ`!
 
 This is similar in nature to `List.orderedInsert`, but note that we increment one of the element
 every time we perform an exchange, making it a different construction. -/
+@[local grind]
 def simplicialInsert (a : ℕ) : List ℕ → List ℕ
   | [] => [a]
   | b :: l => if a < b then a :: b :: l else b :: simplicialInsert (a + 1) l
@@ -121,33 +162,15 @@ def simplicialInsert (a : ℕ) : List ℕ → List ℕ
 /-- `simplicialInsert` just adds one to the length. -/
 lemma simplicialInsert_length (a : ℕ) (L : List ℕ) :
     (simplicialInsert a L).length = L.length + 1 := by
-  induction L generalizing a with
-  | nil => rfl
-  | cons head tail h_rec =>
-    dsimp only [simplicialInsert, List.length_cons]
-    split_ifs with h <;> simp only [List.length_cons, h_rec (a + 1)]
+  induction L generalizing a <;> grind
 
 /-- `simplicialInsert` preserves admissibility -/
 theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ)
-    (hj : j < m + 1) :
+    (hj : j ≤ m) :
     IsAdmissible m <| simplicialInsert j L := by
   induction L generalizing j m with
-  | nil => constructor <;> simp [simplicialInsert, j.le_of_lt_add_one hj]
-  | cons a L h_rec =>
-    dsimp only [simplicialInsert]
-    split_ifs with ha
-    · exact .cons _ hL _ (j.le_of_lt_add_one hj) (fun _ ↦ ha)
-    · refine IsAdmissible.cons _ ?_ _ (not_lt.mp ha |>.trans <| j.le_of_lt_add_one hj) ?_
-      · refine h_rec _ (.tail a L hL) _ (by simp [hj])
-      · rw [not_lt, Nat.le_iff_lt_add_one] at ha
-        intro u
-        cases L with
-        | nil => simp [simplicialInsert, ha]
-        | cons a' l' =>
-          dsimp only [simplicialInsert]
-          split_ifs
-          · exact ha
-          · exact (List.sorted_cons_cons.mp hL.sorted).1
+  | nil => exact IsAdmissible.singleton hj
+  | cons a L h_rec => cases L <;> grind
 
 end AdmissibleLists
 
@@ -194,23 +217,21 @@ Rather than defining it as such, we define it inductively for less painful induc
 It is expected to produce the correct result only if `L` is admissible, and values for
 non-admissible lists should be considered junk values. Similarly, values for out-of-bounds inputs
 are junk values. -/
+@[local grind]
 def simplicialEvalσ (L : List ℕ) : ℕ → ℕ :=
   fun j ↦ match L with
   | [] => j
   | a :: L => if a < simplicialEvalσ L j then simplicialEvalσ L j - 1 else simplicialEvalσ L j
 
-lemma simplicialEvalσ_of_lt_mem (j : ℕ) (hj : ∀ k ∈ L, j ≤ k) : simplicialEvalσ L j = j := by
-  induction L with
-  | nil => grind [simplicialEvalσ]
-  | cons _ _ _ =>
-    simp only [List.mem_cons, forall_eq_or_imp] at hj
-    grind [simplicialEvalσ]
+@[grind ←]
+lemma simplicialEvalσ_of_le_mem (j : ℕ) (hj : ∀ k ∈ L, j ≤ k) : simplicialEvalσ L j = j := by
+  induction L with | nil => grind | cons _ _ _ => simp only [List.forall_mem_cons] at hj; grind
+
+@[deprecated  (since := "2025-10-16")]
+alias simplicialEvalσ_of_lt_mem := simplicialEvalσ_of_le_mem
 
 lemma simplicialEvalσ_monotone (L : List ℕ) : Monotone (simplicialEvalσ L) := by
-  intro a b hab
-  induction L generalizing a b with
-  | nil => exact hab
-  | cons head tail h_rec => grind [simplicialEvalσ]
+  induction L <;> grind [Monotone]
 
 variable {m}
 /- We prove that `simplicialEvalσ` is indeed a lift of
@@ -236,7 +257,7 @@ lemma simplicialEvalσ_of_isAdmissible
       · simp only [Fin.lt_def, Fin.coe_castSucc, IsAdmissible.head_val] at h₁; grind
       · simp only [Fin.lt_def, Fin.coe_castSucc, IsAdmissible.head_val, not_lt] at h₁; grind
       · rfl
-    have := h_rec _ _ hL.tail (by grind) hj
+    have := h_rec _ _ hL.of_cons (by grind) hj
     have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop
     simpa only [toSimplexCategory_obj_mk, SimplexCategory.len_mk, standardσ_cons, Functor.map_comp,
       toSimplexCategory_map_σ, SimplexCategory.σ, SimplexCategory.mkHom,
@@ -260,8 +281,7 @@ lemma standardσ_simplicialInsert (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj :
       have : a < m + 2 := by grind -- helps grind below
       have : σ (Fin.ofNat (m + 2) a) ≫ σ (.ofNat _ j) = σ (.ofNat _ (j + 1)) ≫ σ (.ofNat _ a) := by
         convert σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind
-      simp only [standardσ_cons, Category.assoc, this,
-        h_rec hL.tail (j + 1) (by grind) (by grind)]
+      grind [standardσ_cons]
 
 attribute [local grind] simplicialInsert_length simplicialInsert_isAdmissible in
 /-- Using `standardσ_simplicialInsert`, we can prove that every morphism satisfying `P_σ` is equal
@@ -277,8 +297,8 @@ theorem exists_normal_form_P_σ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf
     rfl
   | of f hf =>
     cases hf with | @σ m k =>
-    use [k.val], m, 1 , rfl, rfl, rfl
-    constructor <;> simp [IsAdmissible, Nat.le_of_lt_add_one k.prop, standardσ]
+    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
+    simp [standardσ]
   | @comp_of _ j x' g g' hg hg' h_rec =>
     cases hg' with | @σ m k =>
     obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
@@ -292,40 +312,23 @@ theorem exists_normal_form_P_σ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf
 
 section MemIsAdmissible
 
+@[grind]
+lemma IsAdmissible.simplicialEvalσ_succ_getElem (hL : IsAdmissible m L)
+    {k : ℕ} {hk : k < L.length} : simplicialEvalσ L L[k] = simplicialEvalσ L (L[k] + 1) := by
+  induction L generalizing m k <;> grind
+
 lemma mem_isAdmissible_of_lt_and_eval_eq_eval_add_one (hL : IsAdmissible m L)
     (j : ℕ) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)) :
     j ∈ L := by
   induction L generalizing m with
-  | nil => grind [simplicialEvalσ]
+  | nil => grind
   | cons a L h_rec =>
-    have := h_rec hL.tail (by grind)
-    suffices ¬j = a → (simplicialEvalσ L j = simplicialEvalσ L (j + 1)) by grind
-    intro hja
-    simp only [simplicialEvalσ] at hj₂
-    have : simplicialEvalσ L j ≤ simplicialEvalσ L (j + 1) :=
-      simplicialEvalσ_monotone L (by grind)
-    suffices ¬a < simplicialEvalσ L j → a < simplicialEvalσ L (j + 1) →
-      simplicialEvalσ L j = simplicialEvalσ L (j + 1) - 1 →
-      simplicialEvalσ L j = simplicialEvalσ L (j + 1) by grind
-    intro h₁ h₂ hj₂
-    simp only [IsAdmissible, List.sorted_cons, List.length_cons] at hL
-    obtain h | rfl | h := Nat.lt_trichotomy j a
-    · grind [simplicialEvalσ_monotone, Monotone, simplicialEvalσ_of_lt_mem]
-    · grind
-    · have := simplicialEvalσ_of_lt_mem L (a + 1) <| fun x h ↦ hL.1.1 x h
-      grind [simplicialEvalσ_monotone, Monotone]
+    have := simplicialEvalσ_monotone L (a := a + 1)
+    rcases lt_trichotomy j a with h | h | h <;> grind
 
 lemma lt_and_eval_eq_eval_add_one_of_mem_isAdmissible (hL : IsAdmissible m L) (j : ℕ) (hj : j ∈ L) :
     j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1) := by
-  induction L generalizing m with
-  | nil => grind
-  | cons a L h_rec =>
-    constructor
-    · grind [List.mem_iff_getElem, IsAdmissible, List.sorted_cons]
-    · obtain rfl | h := List.mem_cons.mp hj
-      · grind [simplicialEvalσ_of_lt_mem, simplicialEvalσ, IsAdmissible, List.sorted_cons]
-      · have := h_rec hL.tail h
-        grind [simplicialEvalσ]
+  grind [List.mem_iff_getElem]
 
 /-- We can characterize elements in an admissible list as exactly those for which
 `simplicialEvalσ` takes the same value twice in a row. -/
diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean
index 66a788265d6011..9bdcbaa7160422 100644
--- a/Mathlib/Data/List/Chain.lean
+++ b/Mathlib/Data/List/Chain.lean
@@ -88,8 +88,6 @@ theorem IsChain.iff_mem_mem_tail {l : List α} :
 @[deprecated (since := "2025-09-24")] alias Chain'.iff_mem := IsChain.iff_mem
 @[deprecated (since := "2025-09-24")] alias Chain.iff_mem := IsChain.iff_mem_mem_tail
 
-@[deprecated (since := "2025-09-24")] alias isChain_cons := isChain_cons_cons
-
 theorem isChain_pair {x y} : IsChain R [x, y] ↔ R x y := by
   simp only [IsChain.singleton, isChain_cons_cons, and_true]
 
@@ -272,8 +270,14 @@ protected theorem IsChain.rel_cons [Trans R R R] (hl : (a :: l).IsChain R) (hb :
 @[deprecated (since := "2025-09-19")]
 alias Chain.rel := IsChain.rel_cons
 
-theorem IsChain.tail {l : List α} : IsChain R l → IsChain R l.tail := by
-  induction l using twoStepInduction <;> grind
+theorem IsChain.of_cons {x} : ∀ {l : List α}, IsChain R (x :: l) → IsChain R l
+  | [] => fun _ => IsChain.nil
+  | _ :: _ => fun | .cons_cons _ h => h
+
+theorem IsChain.tail {l : List α} (h : IsChain R l) : IsChain R l.tail := by
+  cases l
+  · exact IsChain.nil
+  · exact h.of_cons
 
 @[deprecated (since := "2025-09-24")] alias Chain'.tail := IsChain.tail
 
@@ -288,31 +292,33 @@ theorem IsChain.rel_head? {x l} (h : IsChain R (x :: l)) ⦃y⦄ (hy : y ∈ hea
 
 @[deprecated (since := "2025-09-24")] alias Chain'.rel_head? := IsChain.rel_head?
 
-theorem IsChain.cons' {x} : ∀ {l : List α}, IsChain R l → (∀ y ∈ l.head?, R x y) →
+theorem IsChain.cons {x} : ∀ {l : List α}, IsChain R l → (∀ y ∈ l.head?, R x y) →
     IsChain R (x :: l)
   | [], _, _ => .singleton x
   | _ :: _, hl, H => hl.cons_cons <| H _ rfl
 
-@[deprecated (since := "2025-09-24")] alias Chain'.cons' := IsChain.cons'
+@[deprecated (since := "2025-10-16")] alias IsChain.cons' := IsChain.cons
+@[deprecated (since := "2025-09-24")] alias Chain'.cons' := IsChain.cons
 
 lemma IsChain.cons_of_ne_nil {x : α} {l : List α} (l_ne_nil : l ≠ [])
     (hl : IsChain R l) (h : R x (l.head l_ne_nil)) : IsChain R (x :: l) := by
-  refine hl.cons' fun y hy ↦ ?_
+  refine hl.cons fun y hy ↦ ?_
   convert h
   simpa [l.head?_eq_head l_ne_nil] using hy.symm
 
 @[deprecated (since := "2025-09-24")] alias Chain'.cons_of_ne_nil := IsChain.cons_of_ne_nil
 
-theorem isChain_cons' {x l} : IsChain R (x :: l) ↔ (∀ y ∈ head? l, R x y) ∧ IsChain R l :=
-  ⟨fun h => ⟨h.rel_head?, h.tail⟩, fun ⟨h₁, h₂⟩ => h₂.cons' h₁⟩
+theorem isChain_cons {x l} : IsChain R (x :: l) ↔ (∀ y ∈ head? l, R x y) ∧ IsChain R l :=
+  ⟨fun h => ⟨h.rel_head?, h.tail⟩, fun ⟨h₁, h₂⟩ => h₂.cons h₁⟩
 
-@[deprecated (since := "2025-09-24")] alias chain'_cons' := isChain_cons'
+@[deprecated (since := "2025-10-16")] alias isChain_cons' := isChain_cons
+@[deprecated (since := "2025-09-24")] alias chain'_cons' := isChain_cons
 
 theorem isChain_append :
     ∀ {l₁ l₂ : List α},
       IsChain R (l₁ ++ l₂) ↔ IsChain R l₁ ∧ IsChain R l₂ ∧ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y
   | [], l => by simp
-  | [a], l => by simp [isChain_cons', and_comm]
+  | [a], l => by simp [isChain_cons, and_comm]
   | a :: b :: l₁, l₂ => by
     rw [cons_append, cons_append, isChain_cons_cons, isChain_cons_cons,
       ← cons_append, isChain_append, and_assoc]
@@ -432,7 +438,7 @@ theorem isChain_attachWith {l : List α} {p : α → Prop} (h : ∀ x ∈ l, p x
   induction l with
   | nil => grind
   | cons a l IH =>
-    rw [attachWith_cons, isChain_cons', isChain_cons', IH, and_congr_left]
+    rw [attachWith_cons, isChain_cons, isChain_cons, IH, and_congr_left]
     simp_rw [head?_attachWith]
     intros
     constructor <;>
@@ -664,7 +670,7 @@ theorem Acc.list_chain' {l : List.chains r} (acc : ∀ a ∈ l.val.head?, Acc r
   induction acc generalizing l with
   | intro a _ ih =>
     /- Bundle l with a proof that it is r-decreasing to form l' -/
-    have hl' := (List.isChain_cons'.1 hl).2
+    have hl' := (List.isChain_cons.1 hl).2
     let l' : List.chains r := ⟨l, hl'⟩
     have : Acc (List.lex_chains r) l' := by
       rcases l with - | ⟨b, l⟩
@@ -682,7 +688,7 @@ theorem Acc.list_chain' {l : List.chains r} (acc : ∀ a ∈ l.val.head?, Acc r
       rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
       · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
       · apply ih b hr
-      · apply ihl ⟨m, (List.isChain_cons'.1 hm).2⟩ hr
+      · apply ihl ⟨m, (List.isChain_cons.1 hm).2⟩ hr
 
 /-- If `r` is well-founded, the lexicographic order on `r`-decreasing chains is also. -/
 theorem WellFounded.list_chain' (hwf : WellFounded r) :
diff --git a/Mathlib/Data/List/SplitBy.lean b/Mathlib/Data/List/SplitBy.lean
index 877ec48fd8bad0..4fd9b890b622c4 100644
--- a/Mathlib/Data/List/SplitBy.lean
+++ b/Mathlib/Data/List/SplitBy.lean
@@ -86,11 +86,11 @@ private theorem isChain_of_mem_splitByLoop {r : α → α → Bool} {l : List α
     · exact (not_mem_nil hm).elim
     · apply List.isChain_reverse.1
       rw [reverse_reverse]
-      exact isChain_cons'.2 ⟨hga, hg⟩
+      exact isChain_cons.2 ⟨hga, hg⟩
   | cons b l IH =>
     simp only [splitBy.loop, reverse_cons] at h
     split at h
-    · apply IH _ (isChain_cons'.2 ⟨hga, hg⟩) h
+    · apply IH _ (isChain_cons.2 ⟨hga, hg⟩) h
       intro b hb
       rw [head?_cons, Option.mem_some_iff] at hb
       rwa [← hb]
@@ -98,7 +98,7 @@ private theorem isChain_of_mem_splitByLoop {r : α → α → Bool} {l : List α
       obtain rfl | hm := h
       · apply List.isChain_reverse.1
         rw [reverse_append, reverse_cons, reverse_nil, nil_append, reverse_reverse]
-        exact isChain_cons'.2 ⟨hga, hg⟩
+        exact isChain_cons.2 ⟨hga, hg⟩
       · apply IH _ isChain_nil hm
         rintro _ ⟨⟩
 
@@ -122,7 +122,7 @@ private theorem isChain_getLast_head_splitByLoop {r : α → α → Bool} (l : L
   | nil =>
     rw [splitBy.loop, reverse_cons]
     apply List.isChain_reverse.1
-    simpa using isChain_cons'.2 ⟨hga, hgs⟩
+    simpa using isChain_cons.2 ⟨hga, hgs⟩
   | cons b l IH =>
     rw [splitBy.loop]
     split
@@ -134,7 +134,7 @@ private theorem isChain_getLast_head_splitByLoop {r : α → α → Bool} (l : L
     · apply IH
       · simpa using hgs'
       · rw [reverse_cons]
-        apply isChain_cons'.2 ⟨hga, hgs⟩
+        apply isChain_cons.2 ⟨hga, hgs⟩
       · simpa
 
 theorem isChain_getLast_head_splitBy (r : α → α → Bool) (l : List α) :
diff --git a/Mathlib/Data/Nat/Fib/Zeckendorf.lean b/Mathlib/Data/Nat/Fib/Zeckendorf.lean
index a3c6243c2d9e15..0812095b2f8d91 100644
--- a/Mathlib/Data/Nat/Fib/Zeckendorf.lean
+++ b/Mathlib/Data/Nat/Fib/Zeckendorf.lean
@@ -137,7 +137,7 @@ lemma isZeckendorfRep_zeckendorf : ∀ n, (zeckendorf n).IsZeckendorfRep
   | 0 => by simp only [zeckendorf_zero, IsZeckendorfRep_nil]
   | n + 1 => by
     rw [zeckendorf_succ, IsZeckendorfRep, List.cons_append]
-    refine (isZeckendorfRep_zeckendorf _).cons' (fun a ha ↦ ?_)
+    refine (isZeckendorfRep_zeckendorf _).cons (fun a ha ↦ ?_)
     obtain h | h := eq_zero_or_pos (n + 1 - fib (greatestFib (n + 1)))
     · simp only [h, zeckendorf_zero, nil_append, head?_cons, Option.mem_some_iff] at ha
       subst ha
diff --git a/Mathlib/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean
index 80273a4561931e..12ee35bdae65a2 100644
--- a/Mathlib/GroupTheory/CoprodI.lean
+++ b/Mathlib/GroupTheory/CoprodI.lean
@@ -315,7 +315,7 @@ def cons {i} (m : M i) (w : Word M) (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1) :
       rintro l (rfl | hl)
       · exact h1
       · exact w.ne_one l hl
-    chain_ne := w.chain_ne.cons' (fstIdx_ne_iff.mp hmw) }
+    chain_ne := w.chain_ne.cons (fstIdx_ne_iff.mp hmw) }
 
 @[simp]
 theorem fstIdx_cons {i} (m : M i) (w : Word M) (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1) :
@@ -379,7 +379,7 @@ def consRecOn {motive : Word M → Sort*} (w : Word M) (empty : motive empty)
   | nil => exact empty
   | cons m w ih =>
     refine cons m.1 m.2 ⟨w, fun _ hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩ ?_ ?_ (ih _ _)
-    · rw [List.isChain_cons'] at h2
+    · rw [List.isChain_cons] at h2
       simp only [fstIdx, ne_eq, Option.map_eq_some_iff,
         Sigma.exists, exists_and_right, exists_eq_right, not_exists]
       intro m' hm'
diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean
index f7aa9ed85532ce..1324ac014cf55a 100644
--- a/Mathlib/GroupTheory/HNNExtension.lean
+++ b/Mathlib/GroupTheory/HNNExtension.lean
@@ -279,7 +279,7 @@ def cons (g : G) (u : ℤˣ) (w : NormalWord d) (h1 : w.head ∈ d.set u)
       · exact h1
       · exact w.mem_set _ _ h'
     chain := by
-      refine List.isChain_cons'.2 ⟨?_, w.chain⟩
+      refine List.isChain_cons.2 ⟨?_, w.chain⟩
       rintro ⟨u', g'⟩ hu' hw1
       exact h2 _ (by simp_all) hw1 }
 
@@ -299,9 +299,9 @@ def consRecOn {motive : NormalWord d → Sort*} (w : NormalWord d)
       { head := a.2
         toList := l
         mem_set := fun _ _ h => mem_set _ _ (List.mem_cons_of_mem _ h),
-        chain := (List.isChain_cons'.1 chain).2 }
+        chain := (List.isChain_cons.1 chain).2 }
       (mem_set a.1 a.2 List.mem_cons_self)
-      (by simpa using (List.isChain_cons'.1 chain).1)
+      (by simpa using (List.isChain_cons.1 chain).1)
       (ih _ _ _)
 
 @[simp]
@@ -635,7 +635,7 @@ theorem exists_normalWord_prod_eq
          mem_set := by simp
          chain := List.isChain_nil }, by simp⟩
   | cons a l ih =>
-    rcases ih (List.isChain_cons'.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩
+    rcases ih (List.isChain_cons.1 chain).2 with ⟨w', hw'1, hw'2, hw'3⟩
     clear ih
     refine ⟨(t^(a.1 : ℤ) * of a.2 : HNNExtension G A B φ) • w', ?_, ?_⟩
     · rw [prod_smul, hw'1]
@@ -651,7 +651,7 @@ theorem exists_normalWord_prod_eq
         rw [mul_mem_cancel_right this] at hS
         have : a.fst = -a.fst := by
           have hl : l ≠ [] := by rintro rfl; simp_all
-          have : a.fst = (l.head hl).fst := (List.isChain_cons'.1 chain).1 (l.head hl)
+          have : a.fst = (l.head hl).fst := (List.isChain_cons.1 chain).1 (l.head hl)
             (List.head?_eq_head _) hS
           rwa [List.head?_eq_head hl, Option.map_some, ← this, Option.some_inj] at hx'
         simp at this
diff --git a/Mathlib/Order/Height.lean b/Mathlib/Order/Height.lean
index 673f291fc938c3..d54c0c4d842200 100644
--- a/Mathlib/Order/Height.lean
+++ b/Mathlib/Order/Height.lean
@@ -66,7 +66,7 @@ variable {s} {l : List α} {a : α}
 
 theorem cons_mem_subchain_iff :
     (a::l) ∈ s.subchain ↔ a ∈ s ∧ l ∈ s.subchain ∧ ∀ b ∈ l.head?, a < b := by
-  simp only [subchain, mem_setOf_eq, forall_mem_cons, isChain_cons', and_left_comm, and_comm,
+  simp only [subchain, mem_setOf_eq, forall_mem_cons, isChain_cons, and_left_comm, and_comm,
     and_assoc]
 
 @[simp]
@@ -270,7 +270,7 @@ theorem chainHeight_insert_of_forall_gt (a : α) (hx : ∀ b ∈ s, a < b) :
       exacts [(hy _ hi).ne h', not_le_of_gt (hy _ hi) (hx _ h').le]
   · intro l hl
     refine ⟨a::l, ⟨?_, ?_⟩, by simp⟩
-    · rw [isChain_cons']
+    · rw [isChain_cons]
       exact ⟨fun y hy ↦ hx _ (hl.2 _ (mem_of_mem_head? hy)), hl.1⟩
     · rintro x (_ | _)
       exacts [Or.inl (Set.mem_singleton a), Or.inr (hl.2 x ‹x ∈ l›)]
diff --git a/Mathlib/Topology/Category/Profinite/Nobeling/Span.lean b/Mathlib/Topology/Category/Profinite/Nobeling/Span.lean
index 5890cb2b35a061..cfe4ff9875b0d4 100644
--- a/Mathlib/Topology/Category/Profinite/Nobeling/Span.lean
+++ b/Mathlib/Topology/Category/Profinite/Nobeling/Span.lean
@@ -188,7 +188,7 @@ theorem GoodProducts.spanFin [WellFoundedLT I] :
   | cons a as ih =>
     rw [List.map_cons, List.prod_cons]
     intro ha
-    specialize ih (by rw [List.isChain_cons'] at ha; exact ha.2)
+    specialize ih (by rw [List.isChain_cons] at ha; exact ha.2)
     rw [Finsupp.mem_span_image_iff_linearCombination] at ih
     simp only [Finsupp.mem_supported, Finsupp.linearCombination_apply] at ih
     obtain ⟨c, hc, hc'⟩ := ih
diff --git a/scripts/nolints_prime_decls.txt b/scripts/nolints_prime_decls.txt
index 107e89dc8a54d9..159231ffff8134 100644
--- a/scripts/nolints_prime_decls.txt
+++ b/scripts/nolints_prime_decls.txt
@@ -2346,8 +2346,7 @@ List.aestronglyMeasurable_prod'
 List.alternatingProd_cons'
 List.alternatingProd_cons_cons'
 list_casesOn'
-List.isChain_cons'
-List.IsChain.cons'
+
 list_cons'
 List.cons_sublist_cons'
 List.count_cons'