diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean
index 4b8c5588b..56d8424ce 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean
@@ -10,7 +10,6 @@ module
 public import Mathlib.Basic.Finite.Prod
 public import Mathlib.Data.Fintype.Option
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelZeroSpace
-import Mathlib.Basic.Finite.Sum
 
 /-! # Finite-state transducers and their machine semantics
 
@@ -69,14 +68,6 @@ public def toTM : MultiTapeTM 0 Symbol (Q × Option Symbol × Bool) :=
         { inputTape := 0, workTapes := Fin.elim0, output := (τ.final q).head?,
           state := some (q, (τ.final q).tail.head?, true) }
 
-/-- A word of length at most two is its head followed by the head of its tail. -/
-public lemma toList_head?_append {w : List Symbol} (h : w.length ≤ 2) :
-    w.head?.toList ++ w.tail.head?.toList = w := by
-  match w, h with
-  | [], _ => rfl
-  | [_], _ => rfl
-  | [_, _], _ => rfl
-
 variable {input : List Symbol}
 
 /-- The configuration of `τ.toTM` in state `st` with the input head at `pos`, having emitted `o`. -/
@@ -145,7 +136,8 @@ lemma exists_runFrom_halt (q : Q) {i : ℕ} (hi : i ≤ input.length) (o : List
       true ⟨input.length + 1, by omega⟩ (o ++ (τ.final q).head?.toList)
     refine ⟨1 + u + 1, by omega, ⟨input.length + 1, by omega⟩, ?_⟩
     rw [runFrom_add, runFrom_add, runFrom_one, runFrom_one, step_end, hflush, step_halt]
-    rw [List.drop_length, run_nil, List.append_assoc, toList_head?_append (τ.length_final_le q)]
+    rw [List.drop_length, run_nil, List.append_assoc, ← List.take_one, List.head?_tail,
+      ← List.take_add_one, List.take_of_length_le (τ.length_final_le q)]
   | succ n ih =>
     have hi' : i < input.length := by omega
     obtain ⟨u₁, hu₁, hflush⟩ := τ.exists_runFrom_flush (input := input) (τ.step q input[i]).1
@@ -155,7 +147,8 @@ lemma exists_runFrom_halt (q : Q) {i : ℕ} (hi : i ≤ input.length) (o : List
       (o ++ (τ.step q input[i]).2) (by omega)
     refine ⟨1 + u₁ + u₂, by omega, pos, ?_⟩
     rw [runFrom_add, runFrom_add, runFrom_one, step_read _ _ hi', hflush,
-      List.append_assoc, toList_head?_append (τ.length_step_le _ _), hrest,
+      List.append_assoc, ← List.take_one, List.head?_tail, ← List.take_add_one,
+      List.take_of_length_le (τ.length_step_le _ _), hrest,
       List.drop_eq_getElem_cons hi', run_cons, List.append_assoc]
 
 /-- `τ.toTM` emits `τ.run τ.q₀ input` on `input`, in `2 * input.length + 3` steps and zero
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelZipTransducer.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelZipTransducer.lean
index 5cd4d841c..604254c6a 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelZipTransducer.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelZipTransducer.lean
@@ -10,7 +10,6 @@ module
 public import Complexity.Computability.Machines.Turing.MultiTape.Run
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame.Basic
 public import Mathlib.Data.Fintype.Option
-import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
 import Mathlib.Basic.Finite.Prod
 import Mathlib.Basic.Finite.Sum
 
@@ -469,7 +468,8 @@ private lemma seg_zip (q : Q) {r : ℕ} (hr : r ≤ max u.length v.length) (o :
         moveInputPosNat_zero (by omega : 2 * u.length + 2 + v.length ≤ (frame u ++ v).length + 1)]
       exact cfgAt_congr rfl (by omega)
     rw [hu, hv, run_nil_nil]
-    have hfin := Transducer.toList_head?_append (τ.length_final_le q)
+    have hfin := (List.take_add_one (l := τ.final q) (i := 1)).symm
+    rw [List.take_one, ← List.head?_tail, List.take_of_length_le (τ.length_final_le q)] at hfin
     rcases hb : (τ.final q).tail.head? with _ | b
     · rw [hb, Option.toList_none, List.append_nil] at hfin
       rw [hb, Option.map_none] at s₁
@@ -546,7 +546,8 @@ private lemma seg_zip (q : Q) {r : ℕ} (hr : r ≤ max u.length v.length) (o :
       rw [τ.run_of_ne (by simpa [hxdef, hydef, and_comm] using hne), List.tail_drop,
         List.tail_drop, List.append_assoc, List.append_assoc,
         ← List.append_assoc ((τ.step q (y, x)).2.head?.toList),
-        Transducer.toList_head?_append (τ.length_step_le _ _)]
+        ← List.take_one, List.head?_tail, ← List.take_add_one,
+        List.take_of_length_le (τ.length_step_le _ _)]
     rw [hrun]
     exact ((Seg.single (cfgAt_mem_cells (by omega) (by omega)) s₁
       (cfgAt_mem_cells (by omega) (by omega))).trans