diff --git a/CslibFrontier/Algorithms/Lean/LempelZiv/LZ78.lean b/CslibFrontier/Algorithms/Lean/LempelZiv/LZ78.lean
index 297cc84dba..f4ee0b6fc2 100644
--- a/CslibFrontier/Algorithms/Lean/LempelZiv/LZ78.lean
+++ b/CslibFrontier/Algorithms/Lean/LempelZiv/LZ78.lean
@@ -404,8 +404,7 @@ theorem decodePairs_encodePhrases (dict ws : List (List α)) (ht : IsTreeStructu
     obtain ⟨⟨q, hq, a, rfl⟩, ht⟩ := (isTreeStructured_cons _ _ _).1 ht
     simp only [encodePhrases, List.getLast?_concat, List.dropLast_concat, decodePairs]
     have hidx : ([] :: dict).getD (([] :: dict).idxOf q) [] = q := by
-      rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (List.idxOf_lt_length_of_mem hq),
-        Option.getD_some, List.getElem_idxOf]
+      rw [List.getD_eq_getElem?_getD, List.getElem?_idxOf hq, Option.getD_some]
     rw [hidx, ih _ ht]
 
 /-- **The LZ78 code is lossless.** -/
diff --git a/CslibFrontier/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean b/CslibFrontier/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean
index df36c4e703..0799e691a2 100644
--- a/CslibFrontier/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean
+++ b/CslibFrontier/Computability/Circuit/Frontier/TensorNetwork/Explicit.lean
@@ -256,9 +256,8 @@ theorem entry_explicitTable [Zero R] (v : V) (x : Fin m → Bool) :
   simp only [explicitTable, List.getElem_map, List.getElem_range]
   refine N.tensor_congr v _ _ fun e he => ?_
   have hmem : ee e ∈ ps := (N.mem_explicitPorts ee).mpr (by simpa using he)
-  have hidx := List.idxOf_lt_length_of_mem hmem
-  rw [BitString.testBit_lsbValue, List.getD_eq_getElem _ _ (by simpa using hidx), List.getElem_map,
-    List.getElem_idxOf hidx, Function.comp_apply]
+  rw [BitString.testBit_lsbValue]
+  simp [ps, List.getD_eq_getElem?_getD, hmem]
 
 /-- An edge is a port of a vertex at most once. -/
 theorem nodup_explicitPorts (v : V) : (N.explicitPorts ee v).Nodup :=
diff --git a/CslibFrontier/Computability/Circuit/Quantum/PathNetwork.lean b/CslibFrontier/Computability/Circuit/Quantum/PathNetwork.lean
index ff06f8a1a1..a35fd2741d 100644
--- a/CslibFrontier/Computability/Circuit/Quantum/PathNetwork.lean
+++ b/CslibFrontier/Computability/Circuit/Quantum/PathNetwork.lean
@@ -549,9 +549,8 @@ private theorem entry_gateVertex (neg : R) (X : List Bool) (gs : List GateCode)
       simp only [Option.map_some, BitString.testBit_lsbValue]
       have hmem : 2 * (c * (occurrences gs).length + w) + 1 ∈ gatePorts gs c i :=
         List.mem_append_right _ (List.mem_filterMap.mpr ⟨j, hj, by simp [inPort, hl]⟩)
-      have hlt := List.idxOf_lt_length_of_mem hmem
-      rw [List.getD_eq_getElem _ _ (by simpa using hlt), List.getElem_map,
-        List.getElem_idxOf hlt]
+      rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_idxOf hmem,
+        Option.map_some, Option.getD_some]
       congr 1
       omega
   · refine List.map_congr_left fun k hk => ?_
diff --git a/CslibFrontier/Computability/Complexity/Classes/NP/Witness.lean b/CslibFrontier/Computability/Complexity/Classes/NP/Witness.lean
index 4d22bbf9a9..56c24a30fa 100644
--- a/CslibFrontier/Computability/Complexity/Classes/NP/Witness.lean
+++ b/CslibFrontier/Computability/Complexity/Classes/NP/Witness.lean
@@ -217,9 +217,7 @@ private theorem toFinset_selectDistinct_map_append {l : List γ} {S : Finset γ}
   have hget : ∀ v ∈ l,
       (l.map (fun v => decide (v ∈ S)) ++ u).getD (l.idxOf v) false = decide (v ∈ S) := by
     intro v hv
-    have hlt : l.idxOf v < l.length := List.idxOf_lt_length_iff.2 hv
-    rw [List.getD_append _ _ _ _ (by simpa using hlt),
-      List.getD_eq_getElem _ _ (by simpa using hlt), List.getElem_map, List.getElem_idxOf hlt]
+    simp [List.getD_eq_getElem?_getD, List.getElem?_append_left, List.idxOf_lt_length_iff.2 hv]
   ext v
   rw [List.mem_toFinset, mem_selectDistinct]
   exact ⟨fun ⟨hv, h⟩ => of_decide_eq_true ((hget v hv).symm.trans h),
diff --git a/CslibFrontier/Computability/Complexity/Classes/PCP/NP.lean b/CslibFrontier/Computability/Complexity/Classes/PCP/NP.lean
index 6dc20afbd5..6943e2d4a2 100644
--- a/CslibFrontier/Computability/Complexity/Classes/PCP/NP.lean
+++ b/CslibFrontier/Computability/Complexity/Classes/PCP/NP.lean
@@ -133,10 +133,7 @@ theorem tableVerifier_complete (a : α) (proof padding : List Bool)
   apply List.map_congr_left
   intro address haddress
   have hmem := mem_queryTable (BitString.mem_enumList.mp hword) haddress
-  have hindex := List.idxOf_lt_length_of_mem hmem
-  simp only [List.getD_eq_getElem?_getD, List.getElem?_append,
-    List.getElem?_map, List.length_map, hindex, ↓reduceIte, List.getElem?_idxOf hmem,
-    Option.map_some, Option.getD_some]
+  simp [List.getD_eq_getElem?_getD, List.getElem?_append_left, List.idxOf_lt_length_iff.2 hmem]
 
 /-- Every table, including malformed or short certificates, is the restriction of a finite proof.
 The expanded proof is only a mathematical witness; its length need not be polynomial. -/
diff --git a/CslibFrontier/Computability/Complexity/Fagin/Ordered/Completeness.lean b/CslibFrontier/Computability/Complexity/Fagin/Ordered/Completeness.lean
index fa2093af9f..addbff8f4c 100644
--- a/CslibFrontier/Computability/Complexity/Fagin/Ordered/Completeness.lean
+++ b/CslibFrontier/Computability/Complexity/Fagin/Ordered/Completeness.lean
@@ -538,8 +538,7 @@ theorem cnfToOrdered_mem_iff (φ : PL.CNF ℕ) :
       have hi_n : vs.idxOf x < n :=
         lt_of_lt_of_le (lt_of_lt_of_le hi_lt (Nat.le_add_right _ _)) (le_max_right (2 : ℕ) _)
       let v : Fin n := ⟨vs.idxOf x, hi_n⟩
-      have hget_v : vs.getD v.val 0 = x := by
-        rw [List.getD_eq_getElem _ _ hi_lt, List.getElem_idxOf hi_lt]
+      have hget_v : vs.getD v.val 0 = x := by simp [v, List.getD_eq_getElem?_getD, hx_vs]
       have hrel : (FO.cnf.vocabulary.decode (cnfToOrdered φ)).RelMap (FO.cnf.lit b) ![c, v] := by
         refine (relMap_decode_cnfToOrdered φ b c v).mpr ?_
         simp only [cnfToOrderedEntry, vs, hout, ↓reduceIte, decide_eq_true_eq]
diff --git a/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean b/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean
index 27a9e365c5..77d30a143f 100644
--- a/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean
+++ b/CslibFrontier/Computability/Complexity/FineGrained/CountingExponents.lean
@@ -241,12 +241,9 @@ theorem count_eq_modelCount (φ : CNF ℕ) : count φ = φ.modelCount := by
     (fun σ τ _ _ => ?_) (fun i => ?_)
   · constructor
     · intro h v hv
-      have hlt : vs.idxOf v < vs.length :=
-        List.idxOf_lt_length_iff.mpr (CNF.mem_distinctVars.mpr hv)
       have hbit := congrArg (fun n => n.testBit (vs.idxOf v)) (Fin.mk.inj h)
-      simpa only [BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE, List.getD_eq_getElem?_getD,
-        List.getElem?_map, List.getElem?_eq_getElem hlt, List.getElem_idxOf hlt, Option.map_some,
-        Option.getD_some] using hbit
+      simpa [vs, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE, List.getD_eq_getElem?_getD,
+        CNF.mem_distinctVars.mpr hv] using hbit
     · intro h
       have hmap : vs.map σ = vs.map τ :=
         List.map_congr_left fun v hv => h v (CNF.mem_distinctVars.mp hv)
@@ -259,12 +256,8 @@ theorem count_eq_modelCount (φ : CNF ℕ) : count φ = φ.modelCount := by
       exact toNat_ofBoolListLE_bitsAssignment φ.nodup_distinctVars i.isLt
     · rintro ⟨σ, hσ, rfl⟩
       refine (CNF.eval_congr fun v hv => ?_).trans hσ
-      have hidx : vs.idxOf v < vs.length :=
-        List.idxOf_lt_length_iff.mpr (CNF.mem_distinctVars.mpr hv)
-      rw [bitsAssignment, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE,
-        List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_eq_getElem hidx,
-        List.getElem_idxOf hidx]
-      rfl
+      simp [vs, bitsAssignment, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE,
+        List.getD_eq_getElem?_getD, CNF.mem_distinctVars.mpr hv]
 
 open ComputableInPolyTime in
 private theorem computableInPolyTime_init : ComputableInPolyTime init encCNF encState := by
diff --git a/CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean b/CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean
index 58159bec47..23007193fb 100644
--- a/CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean
+++ b/CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean
@@ -307,10 +307,8 @@ theorem graph_mem_iff (hk : cap x = x.k) (hh : (high x).length ≤ cap x) :
       have hva : v ∈ a := (mem_active _).2 ⟨hvl, u, hul, hadj.symm⟩
       have hi := List.idxOf_lt_length_iff.2 hua
       have hj := List.idxOf_lt_length_iff.2 hva
-      have hgi : a.getD (a.idxOf u) 0 = u := by
-        rw [List.getD_eq_getElem _ _ hi, List.getElem_idxOf]
-      have hgj : a.getD (a.idxOf v) 0 = v := by
-        rw [List.getD_eq_getElem _ _ hj, List.getElem_idxOf]
+      have hgi : a.getD (a.idxOf u) 0 = u := by simp [List.getD_eq_getElem?_getD, hua]
+      have hgj : a.getD (a.idxOf v) 0 = v := by simp [List.getD_eq_getElem?_getD, hva]
       have hadj' : (graph ⟨G, k⟩).toSimpleGraph.Adj (a.idxOf u) (a.idxOf v) := by
         refine graph_adj.2 ⟨fun h => hadj.ne (by rw [← hgi, ← hgj, h]), Or.inl ?_⟩
         rw [mem_edges, ← ha, hgi, hgj]
diff --git a/CslibFrontier/Computability/Complexity/Problems/Coloring.lean b/CslibFrontier/Computability/Complexity/Problems/Coloring.lean
index 0c2a62259d..0863720403 100644
--- a/CslibFrontier/Computability/Complexity/Problems/Coloring.lean
+++ b/CslibFrontier/Computability/Complexity/Problems/Coloring.lean
@@ -395,10 +395,8 @@ private theorem gadgetColoring_palette (φ : CNF ℕ) (σ : ℕ → Bool) (c : 
 private theorem gadgetColoring_literal {φ : CNF ℕ} (σ : ℕ → Bool) {l : Literal ℕ}
     (hl : l.1 ∈ φ.vars) : gadgetColoring φ σ (literalVertex φ l) = literalColor σ l := by
   obtain ⟨x, b⟩ := l
-  have hlt : φ.vars.idxOf x < φ.vars.length := List.idxOf_lt_length_iff.2 hl
   simp only [gadgetColoring, literalVertex, Nat.unpair_pair]
-  rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hlt, Option.getD_some,
-    List.getElem_idxOf hlt]
+  rw [List.getD_eq_getElem?_getD, List.getElem?_idxOf hl, Option.getD_some]
   cases b <;> rfl
 
 private theorem gadgetColoring_output (φ : CNF ℕ) (σ : ℕ → Bool) (i j : ℕ) :
diff --git a/CslibFrontier/Computability/Complexity/Problems/Graph/VertexColors.lean b/CslibFrontier/Computability/Complexity/Problems/Graph/VertexColors.lean
index 36de6bcaf7..d87799f9e8 100644
--- a/CslibFrontier/Computability/Complexity/Problems/Graph/VertexColors.lean
+++ b/CslibFrontier/Computability/Complexity/Problems/Graph/VertexColors.lean
@@ -59,9 +59,7 @@ color. -/
 @[simp]
 theorem colorOf_map {G : Graph} {c : ℕ → ℕ} {v : ℕ} (hv : v ∈ G.vertices) :
     colorOf G (G.vertices.map c) v = c v := by
-  have hlt : G.vertices.idxOf v < G.vertices.length := List.idxOf_lt_length_iff.2 hv
-  rw [colorOf, List.getD_eq_getElem _ _ (by simpa using hlt), List.getElem_map,
-    List.getElem_idxOf hlt]
+  simp [colorOf, List.getD_eq_getElem?_getD, hv]
 
 /-- Reading a color from a list of colors is polynomial-time. -/
 @[fun_prop]
diff --git a/CslibFrontier/Computability/Complexity/Problems/Hamiltonian/Directed.lean b/CslibFrontier/Computability/Complexity/Problems/Hamiltonian/Directed.lean
index 7e85082436..8220072f9f 100644
--- a/CslibFrontier/Computability/Complexity/Problems/Hamiltonian/Directed.lean
+++ b/CslibFrontier/Computability/Complexity/Problems/Hamiltonian/Directed.lean
@@ -158,11 +158,9 @@ theorem satisfiable_diamondDetours_iff (φ : CNF ℕ) :
     refine ⟨fun i => σ (φ.vars.getD i 0), fun j hj => ?_⟩
     obtain ⟨l, hl, hσl⟩ := (Clause.eval_eq_true_iff _ _).1
       ((CNF.eval_eq_true_iff _ _).1 hσ φ[j] (List.getElem_mem hj))
-    have hlt := List.idxOf_lt_length_iff.2 (fst_mem_vars hj hl)
     refine ⟨_, mem_diamondDetours.2 ⟨j, hj, l, hl, rfl⟩, rfl, ?_⟩
     simp only
-    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hlt, Option.getD_some,
-      List.getElem_idxOf hlt]
+    rw [List.getD_eq_getElem?_getD, List.getElem?_idxOf (fst_mem_vars hj hl), Option.getD_some]
     exact hσl
 
 /-- **Correctness of the diamond construction.** A formula is satisfiable exactly when its
diff --git a/CslibFrontier/Computability/Complexity/Problems/SAT.lean b/CslibFrontier/Computability/Complexity/Problems/SAT.lean
index 575ae51924..d735a8b7d8 100644
--- a/CslibFrontier/Computability/Complexity/Problems/SAT.lean
+++ b/CslibFrontier/Computability/Complexity/Problems/SAT.lean
@@ -84,10 +84,8 @@ def assignment (φ : CNF ℕ) (w : List Bool) (v : ℕ) : Bool := w.getD (φ.var
 certificate describing `σ` on the variables of `φ`. -/
 theorem assignment_vars_map_append (φ : CNF ℕ) (σ : ℕ → Bool) (w : List Bool) {v : ℕ}
     (hv : v ∈ φ.vars) : assignment φ (φ.vars.map σ ++ w) v = σ v := by
-  have hlt : φ.vars.idxOf v < φ.vars.length := List.idxOf_lt_length_iff.2 hv
-  rw [assignment, List.getD_eq_getElem?_getD, List.getElem?_append_left (by simpa using hlt),
-    List.getElem?_map, List.getElem?_eq_getElem hlt, List.getElem_idxOf hlt]
-  rfl
+  simp [assignment, List.getD_eq_getElem?_getD, List.getElem?_append_left,
+    List.idxOf_lt_length_iff.2 hv]
 
 /-- The values of `σ` listed along the occurrences of `φ` form a certificate describing `σ` on
 the variables of `φ`. -/
diff --git a/CslibFrontier/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean b/CslibFrontier/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean
index e74d1c9af6..fb7f748f19 100644
--- a/CslibFrontier/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean
+++ b/CslibFrontier/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean
@@ -163,8 +163,7 @@ theorem positiveClauseBlock_incidence (φ : CNF ℕ) (d : Graph.OrthogonalDrawin
     exact CNF.mem_vars.mpr ⟨cl, List.fst_mem_of_mem_zipIdx hj, lit.2, hparts.1⟩
   refine ⟨e, he.1, hr, ?_, ?_⟩
   · simp only [hei]
-  · rw [hidx, List.getD_eq_getElem _ _ (List.idxOf_lt_length_of_mem hlvar),
-      List.getElem_idxOf (List.idxOf_lt_length_of_mem hlvar), hl]
+  · rw [hidx, List.getD_eq_getElem?_getD, List.getElem?_idxOf hlvar, Option.getD_some, hl]
 
 /-- Every actual output occurrence has a source-clause owner and a certified local route. -/
 theorem positiveFormulaDrawing_incidence (φ : CNF ℕ) (d : Graph.OrthogonalDrawing)
diff --git a/CslibFrontier/Computability/GenericRAM/Native/HeavyBranchFold.lean b/CslibFrontier/Computability/GenericRAM/Native/HeavyBranchFold.lean
index c666827a16..565d65d192 100644
--- a/CslibFrontier/Computability/GenericRAM/Native/HeavyBranchFold.lean
+++ b/CslibFrontier/Computability/GenericRAM/Native/HeavyBranchFold.lean
@@ -549,9 +549,8 @@ private noncomputable def fiberEquiv {n : ℕ} {S : List ℕ} {vals : List Bool}
     simp only [mergeAssignment, u.2, ↓reduceDIte, Subtype.eta, Equiv.apply_symm_apply, u]
   right_inv := fun ⟨σ, hσ⟩ => by
     apply Subtype.ext; funext i; simp only [mergeAssignment]; split_ifs with hiS
-    · have hk : S.idxOf (i : ℕ) < S.length := List.idxOf_lt_length_of_mem hiS
-      rw [← hσ, List.getD_eq_getElem _ false (by rw [List.length_map]; exact hk)]
-      simp only [List.getElem_map, List.getElem_idxOf hk, extendAssignment_coe]
+    · rw [← hσ]
+      simp [List.getD_eq_getElem?_getD, hiS, extendAssignment_coe]
     · simp only [Equiv.symm_apply_apply]
 
 private theorem evalSystem_mergeAssignment {n : ℕ} {S : List ℕ} {vals : List Bool}
diff --git a/CslibFrontier/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/PairedPorts.lean b/CslibFrontier/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/PairedPorts.lean
index 1b101614bd..0bc93ac095 100644
--- a/CslibFrontier/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/PairedPorts.lean
+++ b/CslibFrontier/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/FairCoin/PairedPorts.lean
@@ -1140,8 +1140,7 @@ theorem clockedOutPort_eq_some_iff (machine : MultiTapePTM k Bool State)
           0 < b / N := ⟨hb_lt, hq_lt, by rw [hb_div]; exact Nat.succ_pos _⟩
       obtain ⟨hp_len, hp_val⟩ := List.getElem?_eq_some_iff.mp hg
       dsimp only [clockedInPort]
-      rw [ite_eq_left hb_cond, hb_mod, ← hq_eq, List.getElem?_eq_getElem hq_len,
-        List.getElem_idxOf hq_len]
+      rw [ite_eq_left hb_cond, hb_mod, ← hq_eq, List.getElem?_idxOf hu_mem]
       simp only [Option.some.injEq, Prod.mk.injEq]
       refine ⟨?_, ?_⟩
       · rw [hb_div, Nat.add_sub_cancel, Nat.mul_comm]
@@ -1183,8 +1182,7 @@ theorem clockedOutPort_eq_some_iff (machine : MultiTapePTM k Bool State)
         ⟨ha_lt, hp_lt, ha_div_lt⟩
       obtain ⟨hq_len, hq_val⟩ := List.getElem?_eq_some_iff.mp hg
       dsimp only [clockedOutPort]
-      rw [ite_eq_left ha_cond, ha_mod, ← hp_eq, List.getElem?_eq_getElem hp_len,
-        List.getElem_idxOf hp_len]
+      rw [ite_eq_left ha_cond, ha_mod, ← hp_eq, List.getElem?_idxOf hv_mem]
       simp only [Option.some.injEq, Prod.mk.injEq]
       refine ⟨?_, ?_⟩
       · have hsub : b / N - 1 + 1 = b / N := by omega
diff --git a/CslibFrontier/Foundations/Combinatorics/BudgetTuples.lean b/CslibFrontier/Foundations/Combinatorics/BudgetTuples.lean
index a5ef26e2b6..44095d4a08 100644
--- a/CslibFrontier/Foundations/Combinatorics/BudgetTuples.lean
+++ b/CslibFrontier/Foundations/Combinatorics/BudgetTuples.lean
@@ -261,9 +261,7 @@ variable {ms}
 private theorem ofList_map (hcover : ∀ Z, Z ∈ ms) (β : M → ℕ) :
     ofList ms (ms.map β) = β := by
   funext Z
-  have hi : ms.idxOf Z < ms.length := List.idxOf_lt_length_iff.mpr (hcover Z)
-  rw [ofList, List.getD_eq_getElem _ _ (by simpa using hi), List.getElem_map,
-    List.getElem_idxOf hi]
+  simp [ofList, List.getD_eq_getElem?_getD, hcover Z]
 
 /-- Listing the values of `ofList ms l` at the coordinates `ms` recovers `l`. -/
 private theorem map_ofList (hms : ms.Nodup) {l : List ℕ} (hl : l.length = ms.length) :
diff --git a/CslibFrontier/Foundations/Data/BitString/List/Positions.lean b/CslibFrontier/Foundations/Data/BitString/List/Positions.lean
index 4222ccfc45..2cc95c5bb1 100644
--- a/CslibFrontier/Foundations/Data/BitString/List/Positions.lean
+++ b/CslibFrontier/Foundations/Data/BitString/List/Positions.lean
@@ -60,9 +60,7 @@ uses its first occurrence, and missing selected bits are false. -/
 theorem getD_readPositions_idxOf {positions : List ℕ} (word : List Bool) {j : ℕ}
     (hj : j ∈ positions) :
     (readPositions positions word).getD (positions.idxOf j) false = word.getD j false := by
-  have hindex : positions.idxOf j < positions.length := List.idxOf_lt_length_iff.mpr hj
-  rw [List.getD_eq_getElem _ _ (by simpa only [length_readPositions] using hindex)]
-  simp [readPositions, List.getElem_idxOf]
+  simp [readPositions, List.getD_eq_getElem?_getD, hj]
 
 /-- Restored bits come from the selected word at selected positions and the reference elsewhere. -/
 theorem getD_restorePositions (positions : List ℕ) (reference bits : List Bool) {j : ℕ}
diff --git a/CslibFrontier/Foundations/LinearAlgebra/Matrix/PairedPorts.lean b/CslibFrontier/Foundations/LinearAlgebra/Matrix/PairedPorts.lean
index 7ac32694c5..7787019e3e 100644
--- a/CslibFrontier/Foundations/LinearAlgebra/Matrix/PairedPorts.lean
+++ b/CslibFrontier/Foundations/LinearAlgebra/Matrix/PairedPorts.lean
@@ -328,21 +328,17 @@ lists satisfying `v ∈ outTargets u ↔ u ∈ inSources v` and covering all non
     · rintro ⟨hout, hq⟩
       have hv_mem : v ∈ outTargets u := List.mem_of_getElem? hout
       have hu_mem : u ∈ inSources v := (hmem_iff u v).mp hv_mem
-      have hq_lt : (inSources v).idxOf u < (inSources v).length :=
-        List.idxOf_lt_length_of_mem hu_mem
       obtain ⟨hp_lt, hp_eq⟩ := List.getElem?_eq_some_iff.mp hout
       refine ⟨?_, ?_⟩
-      · rw [hq, List.getElem?_eq_getElem hq_lt, List.getElem_idxOf hq_lt]
+      · rw [hq, List.getElem?_idxOf hu_mem]
       · rw [← hp_eq]
         exact ((hout_nodup u).idxOf_getElem p.val hp_lt).symm
     · rintro ⟨hin, hp⟩
       have hu_mem : u ∈ inSources v := List.mem_of_getElem? hin
       have hv_mem : v ∈ outTargets u := (hmem_iff u v).mpr hu_mem
-      have hp_lt : (outTargets u).idxOf v < (outTargets u).length :=
-        List.idxOf_lt_length_of_mem hv_mem
       obtain ⟨hq_lt, hq_eq⟩ := List.getElem?_eq_some_iff.mp hin
       refine ⟨?_, ?_⟩
-      · rw [hp, List.getElem?_eq_getElem hp_lt, List.getElem_idxOf hp_lt]
+      · rw [hp, List.getElem?_idxOf hv_mem]
       · rw [← hq_eq]
         exact ((hin_nodup v).idxOf_getElem q.val hq_lt).symm
   outPort_target_injective u {p₁ p₂ v q₁ q₂} h₁ h₂ := by
@@ -371,7 +367,7 @@ lists satisfying `v ∈ outTargets u ↔ u ∈ inSources v` and covering all non
     refine ⟨p, q,
       (listPortLookup_eq_some_iff hin_len (fun a b h => (hmem_iff a b).mp h) u p.val v q).mpr
         ⟨?_, rfl⟩⟩
-    rw [List.getElem?_eq_getElem hp_lt, List.getElem_idxOf hp_lt]
+    exact List.getElem?_idxOf hv
 
 /-- Characterization of `(ofLists ...).outPort u p = some (v, q)`. -/
 theorem ofLists_outPort_eq_some_iff (M : Matrix V V R) (dOut dIn : ℕ)
diff --git a/CslibFrontier/Logics/Propositional/CNF/ModelCount.lean b/CslibFrontier/Logics/Propositional/CNF/ModelCount.lean
index c65a022bf8..f8dc58a124 100644
--- a/CslibFrontier/Logics/Propositional/CNF/ModelCount.lean
+++ b/CslibFrontier/Logics/Propositional/CNF/ModelCount.lean
@@ -171,11 +171,8 @@ theorem exists_lt_two_pow_bitsAssignment_eq {vs : List V} (σ : V → Bool) :
     ∃ i < 2 ^ vs.length, ∀ v ∈ vs, bitsAssignment vs i v = σ v := by
   refine ⟨(BitVec.ofBoolListLE (vs.map σ)).toNat, (BitVec.isLt _).trans_eq (by simp),
     fun v hv => ?_⟩
-  have hlt : vs.idxOf v < vs.length := List.idxOf_lt_length_iff.mpr hv
-  rw [bitsAssignment, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE,
-    List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_eq_getElem hlt,
-    List.getElem_idxOf hlt]
-  rfl
+  simp [bitsAssignment, BitVec.testBit_toNat, BitVec.getLsbD_ofBoolListLE,
+    List.getD_eq_getElem?_getD, hv]
 
 /-- **Satisfiability by exhaustive search.** A formula whose variables are all in the list `vs` is
 satisfiable exactly when it is satisfied by an assignment numbered by some `i < 2 ^ |vs|`. -/
diff --git a/CslibFrontier/Logics/Propositional/CSP/Table/ContractionRows.lean b/CslibFrontier/Logics/Propositional/CSP/Table/ContractionRows.lean
index 50e2ed1dfc..0c66f62e89 100644
--- a/CslibFrontier/Logics/Propositional/CSP/Table/ContractionRows.lean
+++ b/CslibFrontier/Logics/Propositional/CSP/Table/ContractionRows.lean
@@ -80,9 +80,7 @@ theorem deviations_eq_one {reference row : List Bool} {positions : List ℕ}
 theorem project_getD_idxOf (row : List Bool) (positions : List ℕ) {j : ℕ}
     (hj : j ∈ positions) : (project row positions).getD (positions.idxOf j) false =
       row.getD j false := by
-  have hb := List.idxOf_lt_length_iff.mpr hj
-  rw [List.getD_eq_getElem _ _ (by simpa only [project, List.length_map] using hb)]
-  simp only [project, List.getElem_map, List.getElem_idxOf hb]
+  simp [project, List.getD_eq_getElem?_getD, hj]
 
 /-- A full-width row is determined by its outside projection and its internal bits. -/
 theorem eq_of_project_eq_of_eqOn {reference row : List Bool} {positions : List ℕ}
diff --git a/CslibFrontier/Logics/Propositional/ClauseSet/Sparsification/List.lean b/CslibFrontier/Logics/Propositional/ClauseSet/Sparsification/List.lean
index e5893a85d2..cb14a92322 100644
--- a/CslibFrontier/Logics/Propositional/ClauseSet/Sparsification/List.lean
+++ b/CslibFrontier/Logics/Propositional/ClauseSet/Sparsification/List.lean
@@ -565,8 +565,7 @@ theorem mem_dedup {C : Clause V} {l : Literal V} : l ∈ dedup C ↔ l ∈ C :=
   · rintro ⟨i, hi, -⟩
     exact List.mem_of_getElem? (List.mem_zipIdx_iff_getElem?.mp hi)
   · intro hl
-    refine ⟨C.idxOf l, List.mem_zipIdx_iff_getElem?.mpr ?_, rfl⟩
-    rw [List.getElem?_eq_getElem (List.idxOf_lt_length_iff.mpr hl), List.getElem_idxOf]
+    exact ⟨C.idxOf l, List.mem_zipIdx_iff_getElem?.mpr (List.getElem?_idxOf hl), rfl⟩
 
 /-- Literal deduplication yields a duplicate-free clause. -/
 theorem nodup_dedup (C : Clause V) : (dedup C).Nodup := by
diff --git a/manual/machines-and-classes/parameterized-complexity.md b/manual/machines-and-classes/parameterized-complexity.md
index 9ccdf3620a..afabae360a 100644
--- a/manual/machines-and-classes/parameterized-complexity.md
+++ b/manual/machines-and-classes/parameterized-complexity.md
@@ -39,18 +39,18 @@ The forward construction [`hasKernel_of_mem_FPT`](https://github.com/cslib-commu
 
 The target problem has a material convention: [`VertexCover`](../../CslibFrontier/Computability/Complexity/Problems/VertexCover.lean#L105) asks for a cover of **exactly** `k` vertices from the declared vertex set. It is equivalent to an at-most-`k` cover only when `k` does not exceed the number of distinct declared vertices, as stated in [`mem_VertexCover_iff_exists_card_le`](../../CslibFrontier/Computability/Complexity/Problems/VertexCover.lean#L138). A triangle with `k=4` is therefore rejected. The search procedure caps its internal unary search depth by the vertex count and checks that the cap equals the binary target. A huge binary target does not force a correspondingly huge polynomial-time preprocessing loop.
 
-The explicit [`bussKernel`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L465) uses high-degree vertices forced into every small cover, then densely relabels the remaining active vertices. It retains enough isolated vertices to pad a cover to the exact target size. This differs from the at-most-`k` presentation in Cygan et al., Section 2.2.1, where isolated vertices can be discarded. [cygan2015][cygan2015]
+The explicit [`bussKernel`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L462) uses high-degree vertices forced into every small cover, then densely relabels the remaining active vertices. It retains enough isolated vertices to pad a cover to the exact target size. This differs from the at-most-`k` presentation in Cygan et al., Section 2.2.1, where isolated vertices can be discarded. [cygan2015][cygan2015]
 
 The source proves these bounds for every input, including rejected inputs:
 
 | Output quantity | Bound in the original target `k` | Declaration |
 |---|---|---|
-| Listed vertices | `k(k+2)` | [`length_bussKernel_vertices_le`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L624) |
-| Listed edges | `(k(k+1))^2` | [`length_bussKernel_edges_le`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L632) |
-| Encoded instance length | `40(k+1)^6` | [`length_encode_bussKernel_le`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L640) |
-| Output target | `max(k,1)` | [`bussKernel_snd_le`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L660) |
+| Listed vertices | `k(k+2)` | [`length_bussKernel_vertices_le`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L621) |
+| Listed edges | `(k(k+1))^2` | [`length_bussKernel_edges_le`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L629) |
+| Encoded instance length | `40(k+1)^6` | [`length_encode_bussKernel_le`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L637) |
+| Output target | `max(k,1)` | [`bussKernel_snd_le`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L657) |
 
-The fixed rejection instance is an empty graph with target one, explaining the `max(k,1)` allowance. [`computableInPolyTime_bussKernel`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L652) proves native polynomial-time preprocessing under `encVertexCoverInstance`; [`isKernelization_bussKernel`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L668) packages its contract, and [`VertexCover_hasPolyKernel`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L685) concludes a polynomial kernel. These are the actual encoded-size bounds; a smaller literature kernel is not substituted for them.
+The fixed rejection instance is an empty graph with target one, explaining the `max(k,1)` allowance. [`computableInPolyTime_bussKernel`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L648) proves native polynomial-time preprocessing under `encVertexCoverInstance`; [`isKernelization_bussKernel`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L664) packages its contract, and [`VertexCover_hasPolyKernel`](../../CslibFrontier/Computability/Complexity/Parameterized/VertexCover/BussKernel.lean#L680) concludes a polynomial kernel. These are the actual encoded-size bounds; a smaller literature kernel is not substituted for them.
 
 ## Crown decompositions and the linear vertex-cover kernel