From e63cbb627afcebcb1fcc155749887c03a2ba765f Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Wed, 15 Oct 2025 15:57:52 +0100
Subject: [PATCH 01/10] Add improved file

---
 .../GeneratorsRelations/NormalForms.lean      | 190 ++++++++++--------
 Mathlib/Data/List/Chain.lean                  |  32 +--
 Mathlib/Data/Nat/Fib/Zeckendorf.lean          |   2 +-
 Mathlib/GroupTheory/CoprodI.lean              |   2 +-
 scripts/nolints_prime_decls.txt               |   1 -
 5 files changed, 125 insertions(+), 102 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index f02dcd2dddfb53..cb1751536d47f2 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -41,71 +41,101 @@ section AdmissibleLists
 -- easier to perform inductive constructions and proofs on such lists, and we instead bundle
 -- propositions asserting that various List constructions produce admissible lists.
 
-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`.
 -/
-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
+
+section IsAdmissible
+
+variable {m a b : ℕ} {L : List ℕ}
+
+@[simp, grind =]
+theorem isAdmissible_singleton : IsAdmissible m [a] ↔ a ≤ m :=
+    ⟨fun | .singleton h => h, .singleton⟩
+
+@[simp, grind =]
+theorem isAdmissible_cons_cons : IsAdmissible m (a :: b :: L) ↔
+    a < b ∧ IsAdmissible (m + 1) (b :: L) ∧ a ≤ m :=
+  ⟨fun | .cons_cons hab hbL ha => ⟨hab, hbL, ha⟩, fun ⟨hab, hbL, ha⟩ => .cons_cons hab hbL ha⟩
+
+theorem isAdmissible_cons : 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, IH, List.length_cons, and_assoc,
+      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
+    exact fun _ _ => ⟨fun h =>
+      fun | 0 => fun _ => h.1 | k + 1 => fun _ => (h.2 k _).trans (by grind),
+      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩
+
+end IsAdmissible
 
 namespace IsAdmissible
 
-lemma nil : IsAdmissible m [] := by simp [IsAdmissible]
+theorem isChain {m L} (hL : IsAdmissible m L) :
+    L.IsChain (· < ·) := (isAdmissible_iff_isChain_and_le.mp hL).1
 
-variable {m}
+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
 
-lemma sorted {L : List ℕ} (hL : IsAdmissible m L) : L.Sorted (· < ·) := hL.1
+/-- The tail of an `m`-admissible list is (m+1)-admissible. -/
+lemma of_cons {m a L} (h : IsAdmissible m (a :: L)) :
+    IsAdmissible (m + 1) L := by cases L <;> grind
+
+/-- The tail of an `m`-admissible list is (m+1)-admissible. -/
+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
 
 /-- 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)
+lemma head_le {m a L} (hL : IsAdmissible m (a :: L)) :
+    ∀ a' ∈ (a :: L), a ≤ a' := by grind
+
+theorem sorted {m L} (hL : IsAdmissible m L) : L.Sorted (· < ·) := hL.pairwise
+
+lemma getElem_lt {m L} (hL : IsAdmissible m L)
+    {k : ℕ} {hk : k < L.length} : L[k] < m + L.length := by
+  exact (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])
 
 /-- The head of an `m`-admissible list. -/
 @[simps!]
-def head (a : ℕ) (L : List ℕ) (hl : IsAdmissible m (a :: L)) : Fin (m + 1) :=
+def head {m a L} (hl : IsAdmissible m (a :: L)) : Fin (m + 1) :=
   hl.getElemAsFin 0 (by simp)
 
 end IsAdmissible
 
+theorem _root_.List.IsChain.isAdmissible_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₂⟩)
+
 /-- The construction `simplicialInsert` describes inserting an element in a list of integer and
 moving it to its "right place" according to the simplicial relations. Somewhat miraculously,
 the algorithm is the same for the first or the fifth simplicial relations, making it "valid"
@@ -127,27 +157,20 @@ lemma simplicialInsert_length (a : ℕ) (L : List ℕ) :
     dsimp only [simplicialInsert, List.length_cons]
     split_ifs with h <;> simp only [List.length_cons, h_rec (a + 1)]
 
+variable (m)
+
 /-- `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]
+  | nil => exact IsAdmissible.singleton hj
   | cons a L h_rec =>
-    dsimp only [simplicialInsert]
+    simp only [simplicialInsert, apply_ite (IsAdmissible m ·)]
     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
+    · exact hL.cons_cons ha hj
+    · simp_rw [isAdmissible_cons]
+      cases L <;> grind [simplicialInsert]
 
 end AdmissibleLists
 
@@ -199,13 +222,16 @@ def simplicialEvalσ (L : List ℕ) : ℕ → ℕ :=
   | [] => 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
+lemma simplicialEvalσ_of_le_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σ]
 
+@[deprecated  (since := "2025-10-15")]
+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
@@ -236,7 +262,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,
@@ -261,7 +287,7 @@ lemma standardσ_simplicialInsert (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj :
       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)]
+        h_rec hL.of_cons (j + 1) (by grind) (by grind)]
 
 attribute [local grind] simplicialInsert_length simplicialInsert_isAdmissible in
 /-- Using `standardσ_simplicialInsert`, we can prove that every morphism satisfying `P_σ` is equal
@@ -277,8 +303,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 +318,34 @@ theorem exists_normal_form_P_σ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf
 
 section MemIsAdmissible
 
+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 with
+  | nil => grind
+  | cons a L h_rec =>
+    · cases k
+      · grind [simplicialEvalσ, simplicialEvalσ_of_le_mem]
+      · grind [simplicialEvalσ, isAdmissible_cons]
+
 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σ]
   | 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]
+    rcases lt_trichotomy j a with h | h | h
+    · grind [simplicialEvalσ_of_le_mem]
     · grind
-    · have := simplicialEvalσ_of_lt_mem L (a + 1) <| fun x h ↦ hL.1.1 x h
-      grind [simplicialEvalσ_monotone, Monotone]
+    · have := simplicialEvalσ_of_le_mem L (a + 1) (by grind)
+      have := simplicialEvalσ_monotone L (a := a + 1)
+      have := h_rec hL.of_cons (by grind)
+      grind [simplicialEvalσ]
 
 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σ]
+  simp_rw [List.mem_iff_getElem] at hj
+  rcases hj with ⟨k, hk, rfl⟩
+  exact ⟨hL.getElem_lt, hL.simplicialEvalσ_succ_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..9d1388f5639e42 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,31 @@ 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-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-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 +436,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 +668,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 +686,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/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..eea2a44df079d8 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) :
diff --git a/scripts/nolints_prime_decls.txt b/scripts/nolints_prime_decls.txt
index 107e89dc8a54d9..2a27afb8cf5200 100644
--- a/scripts/nolints_prime_decls.txt
+++ b/scripts/nolints_prime_decls.txt
@@ -2347,7 +2347,6 @@ List.alternatingProd_cons'
 List.alternatingProd_cons_cons'
 list_casesOn'
 List.isChain_cons'
-List.IsChain.cons'
 list_cons'
 List.cons_sublist_cons'
 List.count_cons'

From f4d1cba1f4b7d93417118380a31e4048a0c8eb4c Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Wed, 15 Oct 2025 16:03:35 +0100
Subject: [PATCH 02/10] Add equivalency to old definition

---
 .../SimplexCategory/GeneratorsRelations/NormalForms.lean  | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index cb1751536d47f2..81f59fbdcf1f7c 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -82,6 +82,14 @@ theorem isAdmissible_iff_isChain_and_le : IsAdmissible m L ↔
       fun | 0 => fun _ => h.1 | k + 1 => fun _ => (h.2 k _).trans (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_iff_sorted_and_le : IsAdmissible m L ↔
+    L.Sorted (· < ·) ∧ ∀ k, (h : k < L.length) → L[k] ≤ m + k :=
+  isAdmissible_iff_pairwise_and_le
+
 end IsAdmissible
 
 namespace IsAdmissible

From 0e8d03bf4b7e5a886802a0c6fb6fc4341f5c82e7 Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Wed, 15 Oct 2025 16:46:32 +0100
Subject: [PATCH 03/10] Find/replace

---
 .../GeneratorsRelations/NormalForms.lean               |  3 +++
 Mathlib/Data/List/SplitBy.lean                         | 10 +++++-----
 Mathlib/GroupTheory/CoprodI.lean                       |  2 +-
 Mathlib/GroupTheory/HNNExtension.lean                  | 10 +++++-----
 Mathlib/Order/Height.lean                              |  4 ++--
 Mathlib/Topology/Category/Profinite/Nobeling/Span.lean |  2 +-
 scripts/nolints_prime_decls.txt                        |  2 +-
 7 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 81f59fbdcf1f7c..93f364b77db780 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -338,6 +338,9 @@ lemma IsAdmissible.simplicialEvalσ_succ_getElem (hL : IsAdmissible m L)
 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 hL
+  any_goals grind [simplicialEvalσ]
+  
   induction L generalizing m with
   | nil => grind [simplicialEvalσ]
   | cons a L h_rec =>
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/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean
index eea2a44df079d8..12ee35bdae65a2 100644
--- a/Mathlib/GroupTheory/CoprodI.lean
+++ b/Mathlib/GroupTheory/CoprodI.lean
@@ -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 2a27afb8cf5200..159231ffff8134 100644
--- a/scripts/nolints_prime_decls.txt
+++ b/scripts/nolints_prime_decls.txt
@@ -2346,7 +2346,7 @@ List.aestronglyMeasurable_prod'
 List.alternatingProd_cons'
 List.alternatingProd_cons_cons'
 list_casesOn'
-List.isChain_cons'
+
 list_cons'
 List.cons_sublist_cons'
 List.count_cons'

From bba4a50ef2f6c184127daf538d4c4a0e515d2036 Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Wed, 15 Oct 2025 16:47:12 +0100
Subject: [PATCH 04/10] Fix error commited wrongly

---
 .../SimplexCategory/GeneratorsRelations/NormalForms.lean       | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 93f364b77db780..81f59fbdcf1f7c 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -338,9 +338,6 @@ lemma IsAdmissible.simplicialEvalσ_succ_getElem (hL : IsAdmissible m L)
 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 hL
-  any_goals grind [simplicialEvalσ]
-  
   induction L generalizing m with
   | nil => grind [simplicialEvalσ]
   | cons a L h_rec =>

From a0db8ee55806afe556f412fab94960eb5a90a8c5 Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Thu, 16 Oct 2025 10:21:15 +0100
Subject: [PATCH 05/10] Small update

---
 .../GeneratorsRelations/NormalForms.lean             | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 81f59fbdcf1f7c..2091fc66410de4 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -90,7 +90,9 @@ theorem isAdmissible_iff_sorted_and_le : IsAdmissible m L ↔
     L.Sorted (· < ·) ∧ ∀ k, (h : k < L.length) → L[k] ≤ m + k :=
   isAdmissible_iff_pairwise_and_le
 
-end IsAdmissible
+theorem _root_.List.IsChain.isAdmissible_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
 
@@ -138,11 +140,13 @@ def getElemAsFin {m L} (hl : IsAdmissible m L) (k : ℕ)
 def head {m a L} (hl : IsAdmissible m (a :: L)) : Fin (m + 1) :=
   hl.getElemAsFin 0 (by simp)
 
+theorem mono {n} (hmn : m ≤ n) (hL : IsAdmissible m L) : IsAdmissible n L :=
+  hL.isChain.isAdmissible_of_forall_getElem_le
+  fun _ _ => (hL.le _ _).trans <| Nat.add_le_add_right hmn _
+
 end IsAdmissible
 
-theorem _root_.List.IsChain.isAdmissible_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₂⟩)
+end IsAdmissible
 
 /-- The construction `simplicialInsert` describes inserting an element in a list of integer and
 moving it to its "right place" according to the simplicial relations. Somewhat miraculously,

From 59c98d2551312a660ef8326656c30ce511937a51 Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Thu, 16 Oct 2025 10:56:41 +0100
Subject: [PATCH 06/10] Golfs

---
 .../GeneratorsRelations/NormalForms.lean      | 91 ++++++-------------
 1 file changed, 29 insertions(+), 62 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 2091fc66410de4..619b816f21c902 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -42,31 +42,36 @@ section AdmissibleLists
 -- propositions asserting that various List constructions produce admissible lists.
 
 /-- 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.
 -/
 @[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')
+  | 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 : IsAdmissible m [a] ↔ a ≤ m :=
+theorem isAdmissible_singleton_iff : IsAdmissible m [a] ↔ a ≤ m :=
     ⟨fun | .singleton h => h, .singleton⟩
 
 @[simp, grind =]
-theorem isAdmissible_cons_cons : IsAdmissible m (a :: b :: L) ↔
+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⟩, fun ⟨hab, hbL, ha⟩ => .cons_cons hab hbL ha⟩
+  ⟨fun | .cons_cons hab hbL ha => ⟨hab, hbL, ha⟩, by grind⟩
 
-theorem isAdmissible_cons : IsAdmissible m (a :: L) ↔
+theorem isAdmissible_cons_iff : IsAdmissible m (a :: L) ↔
     a ≤ m ∧ ((_ : 0 < L.length) → a < L[0]) ∧ IsAdmissible (m + 1) L := by
   cases L <;> grind
 
@@ -76,7 +81,7 @@ theorem isAdmissible_iff_isChain_and_le : IsAdmissible m L ↔
   | nil => grind
   | singleton _ => simp
   | cons_cons _ _ _ _ IH =>
-    simp_rw [isAdmissible_cons_cons, IH, List.length_cons, and_assoc,
+    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 =>
       fun | 0 => fun _ => h.1 | k + 1 => fun _ => (h.2 k _).trans (by grind),
@@ -86,11 +91,7 @@ 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_iff_sorted_and_le : IsAdmissible m L ↔
-    L.Sorted (· < ·) ∧ ∀ k, (h : k < L.length) → L[k] ≤ m + k :=
-  isAdmissible_iff_pairwise_and_le
-
-theorem _root_.List.IsChain.isAdmissible_of_forall_getElem_le {m L} (hL : L.IsChain (· < ·))
+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₂⟩)
 
@@ -103,12 +104,9 @@ 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. -/
-lemma of_cons {m a L} (h : IsAdmissible m (a :: L)) :
+@[grind →] lemma of_cons {m a L} (h : IsAdmissible m (a :: L)) :
     IsAdmissible (m + 1) L := by cases L <;> grind
 
-/-- The tail of an `m`-admissible list is (m+1)-admissible. -/
-alias tail := IsAdmissible.of_cons
-
 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
 
@@ -120,11 +118,6 @@ theorem pairwise {m L} (hL : IsAdmissible m L) : L.Pairwise (· < ·) :=
 lemma head_lt {m a L} (hL : IsAdmissible m (a :: L)) :
     ∀ a' ∈ L, a < a' := fun _ => L.rel_of_pairwise_cons hL.pairwise
 
-lemma head_le {m a L} (hL : IsAdmissible m (a :: L)) :
-    ∀ a' ∈ (a :: L), a ≤ a' := by grind
-
-theorem sorted {m L} (hL : IsAdmissible m L) : L.Sorted (· < ·) := hL.pairwise
-
 lemma getElem_lt {m L} (hL : IsAdmissible m L)
     {k : ℕ} {hk : k < L.length} : L[k] < m + L.length := by
   exact (hL.le k hk).trans_lt (Nat.add_lt_add_left hk _)
@@ -141,7 +134,7 @@ def head {m a L} (hl : IsAdmissible m (a :: L)) : Fin (m + 1) :=
   hl.getElemAsFin 0 (by simp)
 
 theorem mono {n} (hmn : m ≤ n) (hL : IsAdmissible m L) : IsAdmissible n L :=
-  hL.isChain.isAdmissible_of_forall_getElem_le
+  isAdmissible_of_isChain_of_forall_getElem_le hL.isChain
   fun _ _ => (hL.le _ _).trans <| Nat.add_le_add_right hmn _
 
 end IsAdmissible
@@ -156,6 +149,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
@@ -163,11 +157,7 @@ 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
 
 variable (m)
 
@@ -177,12 +167,7 @@ theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : IsAdmissible (m + 1)
     IsAdmissible m <| simplicialInsert j L := by
   induction L generalizing j m with
   | nil => exact IsAdmissible.singleton hj
-  | cons a L h_rec =>
-    simp only [simplicialInsert, apply_ite (IsAdmissible m ·)]
-    split_ifs with ha
-    · exact hL.cons_cons ha hj
-    · simp_rw [isAdmissible_cons]
-      cases L <;> grind [simplicialInsert]
+  | cons a L h_rec => cases L <;> grind
 
 end AdmissibleLists
 
@@ -229,26 +214,18 @@ 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-bonds 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
 
+@[grind ←]
 lemma simplicialEvalσ_of_le_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σ]
-
-@[deprecated  (since := "2025-10-15")]
-alias simplicialEvalσ_of_lt_mem := simplicialEvalσ_of_le_mem
+  induction L with | nil => grind | cons _ _ _ => simp only [List.forall_mem_cons] at hj; grind
 
 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
@@ -332,26 +309,16 @@ section MemIsAdmissible
 
 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 with
-  | nil => grind
-  | cons a L h_rec =>
-    · cases k
-      · grind [simplicialEvalσ, simplicialEvalσ_of_le_mem]
-      · grind [simplicialEvalσ, isAdmissible_cons]
+  induction L generalizing m k with | nil => grind | cons a L h_rec => cases 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 =>
-    rcases lt_trichotomy j a with h | h | h
-    · grind [simplicialEvalσ_of_le_mem]
-    · grind
-    · have := simplicialEvalσ_of_le_mem L (a + 1) (by grind)
-      have := simplicialEvalσ_monotone L (a := a + 1)
-      have := h_rec hL.of_cons (by grind)
-      grind [simplicialEvalσ]
+    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

From 602cc634ae19c48d82624f351291d0cf22247fc4 Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Thu, 16 Oct 2025 11:02:29 +0100
Subject: [PATCH 07/10] Add deprecations

---
 .../SimplexCategory/GeneratorsRelations/NormalForms.lean | 9 +++++++++
 Mathlib/Data/List/Chain.lean                             | 4 +++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 619b816f21c902..1e2f9f188df8a0 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -107,12 +107,18 @@ theorem le {m} {L : List ℕ} (hL : IsAdmissible m L) : ∀ k (h : k < L.length)
 @[grind →] lemma of_cons {m a L} (h : IsAdmissible m (a :: L)) :
     IsAdmissible (m + 1) L := by cases L <;> grind
 
+@[deprecated (since := "2025-10-15")]
+alias tail := IsAdmissible.of_cons
+
 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` -/
 @[grind →]
 lemma head_lt {m a L} (hL : IsAdmissible m (a :: L)) :
@@ -224,6 +230,9 @@ def simplicialEvalσ (L : List ℕ) : ℕ → ℕ :=
 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
   induction L <;> grind [Monotone]
 
diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean
index 9d1388f5639e42..a8639d44618356 100644
--- a/Mathlib/Data/List/Chain.lean
+++ b/Mathlib/Data/List/Chain.lean
@@ -297,6 +297,7 @@ theorem IsChain.cons {x} : ∀ {l : List α}, IsChain R l → (∀ y ∈ l.head?
   | [], _, _ => .singleton x
   | _ :: _, hl, H => hl.cons_cons <| H _ rfl
 
+@[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 ≠ [])
@@ -309,7 +310,8 @@ lemma IsChain.cons_of_ne_nil {x : α} {l : List α} (l_ne_nil : l ≠ [])
 
 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-10-16")] alias isChain_cons' := isChain_cons
 @[deprecated (since := "2025-09-24")] alias chain'_cons' := isChain_cons
 
 theorem isChain_append :

From 9f07c465f72d88ffb952a2e6a4e810e398b5855c Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Thu, 16 Oct 2025 10:03:10 +0000
Subject: [PATCH 08/10] [pre-commit.ci lite] apply automatic fixes

---
 Mathlib/Data/List/Chain.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean
index a8639d44618356..9bdcbaa7160422 100644
--- a/Mathlib/Data/List/Chain.lean
+++ b/Mathlib/Data/List/Chain.lean
@@ -310,7 +310,7 @@ lemma IsChain.cons_of_ne_nil {x : α} {l : List α} (l_ne_nil : l ≠ [])
 
 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-10-16")] alias isChain_cons' := isChain_cons
 @[deprecated (since := "2025-09-24")] alias chain'_cons' := isChain_cons
 

From b45e2a55784cd8f43b3e4edc72a9af149d787bfe Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Thu, 16 Oct 2025 13:58:14 +0100
Subject: [PATCH 09/10] Grind golfs

---
 .../GeneratorsRelations/NormalForms.lean      | 21 ++++++++-----------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 1e2f9f188df8a0..b58bc3109123ec 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -97,10 +97,10 @@ theorem isAdmissible_of_isChain_of_forall_getElem_le {m L} (hL : L.IsChain (· <
 
 namespace IsAdmissible
 
-theorem isChain {m L} (hL : IsAdmissible m L) :
+@[grind →] theorem isChain {m L} (hL : IsAdmissible m L) :
     L.IsChain (· < ·) := (isAdmissible_iff_isChain_and_le.mp hL).1
 
-theorem le {m} {L : List ℕ} (hL : IsAdmissible m L) : ∀ k (h : k < L.length),
+@[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. -/
@@ -124,7 +124,7 @@ alias sorted := pairwise
 lemma head_lt {m a L} (hL : IsAdmissible m (a :: L)) :
     ∀ a' ∈ L, a < a' := fun _ => L.rel_of_pairwise_cons hL.pairwise
 
-lemma getElem_lt {m L} (hL : IsAdmissible m L)
+@[grind →] lemma getElem_lt {m L} (hL : IsAdmissible m L)
     {k : ℕ} {hk : k < L.length} : L[k] < m + L.length := by
   exact (hL.le k hk).trans_lt (Nat.add_lt_add_left hk _)
 
@@ -132,16 +132,15 @@ lemma getElem_lt {m L} (hL : IsAdmissible m L)
 @[simps]
 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 {m a L} (hl : IsAdmissible m (a :: L)) : Fin (m + 1) :=
-  hl.getElemAsFin 0 (by simp)
+  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 hL.isChain
-  fun _ _ => (hL.le _ _).trans <| Nat.add_le_add_right hmn _
+  isAdmissible_of_isChain_of_forall_getElem_le (by grind) (by grind)
 
 end IsAdmissible
 
@@ -284,8 +283,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.of_cons (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
@@ -316,6 +314,7 @@ 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 with | nil => grind | cons a L h_rec => cases k <;> grind
@@ -331,9 +330,7 @@ lemma mem_isAdmissible_of_lt_and_eval_eq_eval_add_one (hL : IsAdmissible m L)
 
 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
-  simp_rw [List.mem_iff_getElem] at hj
-  rcases hj with ⟨k, hk, rfl⟩
-  exact ⟨hL.getElem_lt, hL.simplicialEvalσ_succ_getElem⟩
+  rw [List.mem_iff_getElem] at hj; grind
 
 /-- We can characterize elements in an admissible list as exactly those for which
 `simplicialEvalσ` takes the same value twice in a row. -/

From 0e7bf6534afac1f797a75e768cb90e193f450a3a Mon Sep 17 00:00:00 2001
From: Wrenna Robson <wrenna.robson@bristol.ac.uk>
Date: Fri, 17 Oct 2025 11:06:53 +0100
Subject: [PATCH 10/10] Fix small issue

---
 .../SimplexCategory/GeneratorsRelations/NormalForms.lean        | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
index 540ae14484aadb..49a5d26c9ae6ed 100644
--- a/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
+++ b/Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms.lean
@@ -164,8 +164,6 @@ lemma simplicialInsert_length (a : ℕ) (L : List ℕ) :
     (simplicialInsert a L).length = L.length + 1 := by
   induction L generalizing a <;> grind
 
-variable (m)
-
 /-- `simplicialInsert` preserves admissibility -/
 theorem simplicialInsert_isAdmissible (L : List ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ)
     (hj : j ≤ m) :